LoopScopeInvRuleTests

1

tests

0

failures

0

ignored

4.752s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticProofOfBenchmarkWithLabeledBreaksAndContinues() 4.752s passed

Standard output

470526     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/standardRules.key 
470528     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ldt.key 
470529     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/boolean.key 
470529     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key 
470531     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerHeader.key 
470532     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatHeader.key 
470532     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/heap.key 
470532     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/locSets.key 
470533     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/permission.key 
470533     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/reach.key 
470533     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seq.key 
470534     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/map.key 
470537     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/freeADT.key 
470537     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wellfound.key 
470538     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/charListHeader.key 
470542     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/propRule.key 
470545     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/firstOrderRules.key 
470549     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ifThenElseRules.key 
470555     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/formulaNormalisationRules.key 
470573     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/updateRules.key 
470578     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerRulesCommon.key 
470582     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRules.key 
470586     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key 
470589     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesCheckedSemantics.key 
470591     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesJavaSemantics.key 
470595     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key 
470648     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
470648     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
470649     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
470649     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
470659     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intDiv.key 
470671     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bsum.key 
470708     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bprod.key 
470724     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/binaryAxioms.key 
470726     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/binaryLemmas.key 
470729     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intPow.key 
470735     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesCommon.key 
470744     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRules.key 
470745     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesVerifyNormal.key 
470745     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesAssumeStrictfp.key 
470751     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/genericRules.key 
470757     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/booleanRules.key 
470759     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/epsilon.key 
470761     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/locSetsRules.key 
470784     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/heapRules.key 
470806     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/permissionRules.key 
470815     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/reachRules.key 
470832     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqCoreRules.key 
470834     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqRules.key 
470855     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqPerm.key 
470871     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqPerm2.key 
470874     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/javaRules.key 
470921     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/assertions.key 
471077     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopRules.key 
471081     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/activeUse.key 
471110     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/instanceAllocation.key 
471119     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/java5.key 
471121     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key 
471140     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key 
471154     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bigint.key 
471161     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
471163     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/adtProgramDecompositionRules.key 
471175     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/precRules.key 
471177     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/charListRules.key 
471188     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExTheory.key 
471189     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExHeader.key 
471189     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExAxioms.key 
471192     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExLemmaProven.key 
471197     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqEq.key 
471202     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/infFlow.key 
471207     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/mapSize.key 
471210     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wd.key 
471211     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdHeader.key 
471212     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdGeneralRules.key 
471214     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdNumericalRules.key 
471231     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdLocSetRules.key 
471237     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdHeapRules.key 
471245     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdReachRules.key 
471246     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdSeqRules.key 
471248     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdStringRules.key 
471250     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdRegExRules.key 
471252     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdFormulaRules.key 
471365     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopInvariantRules.key 
471367     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/forLoopRules.key 
471369     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/execRules.key 
471419     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopScopeRules.key 
471443     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src/test/resources/testcase/loopScopeInvRule/Test.key 
472600     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now /home/runner/work/key/key/key.core/src/test/resources/testcase/loopScopeInvRule/Test.java 
472606     DEBUG Test worker     d.u.i.k.s.TermLabelSettings TermLabelSettings: Failure while reading the setting "UseOriginLabels".Using the default value: true.The string read was: null 
472607     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/home/runner/work/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
474690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.1ns 
474690     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src/test/resources/testcase/loopScopeInvRule/Test.key