MergeRuleTests

11

tests

0

failures

0

ignored

59.738s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 9.702s passed
testDoAutomaticGcdProofWithMergePointStatements() 9.647s passed
testDoManualGcdProof() 16.513s passed
testLoadClosedGcdProofWithMergePointStatements() 3.482s passed
testLoadGcdProof() 3.148s passed
testLoadGcdProofWithPredAbstr() 3.420s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.188s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 2.838s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.662s passed
testMergeIndistinguishablePathConditionsWithITE() 2.556s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.582s passed

Standard output

408543     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/standardRules.key 
408543     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ldt.key 
408543     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/boolean.key 
408543     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key 
408559     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerHeader.key 
408559     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatHeader.key 
408559     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/heap.key 
408559     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/locSets.key 
408559     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/permission.key 
408559     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/reach.key 
408559     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seq.key 
408559     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/map.key 
408559     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/freeADT.key 
408559     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wellfound.key 
408559     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/charListHeader.key 
408559     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/propRule.key 
408559     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/firstOrderRules.key 
408559     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ifThenElseRules.key 
408574     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/formulaNormalisationRules.key 
408590     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/updateRules.key 
408590     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerRulesCommon.key 
408590     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRules.key 
408590     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key 
408590     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesCheckedSemantics.key 
408590     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesJavaSemantics.key 
408606     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key 
408637     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
408637     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
408637     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
408637     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
408653     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intDiv.key 
408653     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bsum.key 
408684     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bprod.key 
408699     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/binaryAxioms.key 
408699     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/binaryLemmas.key 
408699     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intPow.key 
408715     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesCommon.key 
408715     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRules.key 
408715     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesVerifyNormal.key 
408715     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesAssumeStrictfp.key 
408715     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/genericRules.key 
408731     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/booleanRules.key 
408731     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/epsilon.key 
408731     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/locSetsRules.key 
408746     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/heapRules.key 
408762     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/permissionRules.key 
408778     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/reachRules.key 
408793     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqCoreRules.key 
408793     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqRules.key 
408809     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqPerm.key 
408824     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqPerm2.key 
408824     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/javaRules.key 
408856     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/assertions.key 
408965     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopRules.key 
408965     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/activeUse.key 
408981     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/instanceAllocation.key 
408996     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/java5.key 
408996     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key 
409012     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key 
409012     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bigint.key 
409029     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
409030     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/adtProgramDecompositionRules.key 
409036     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/precRules.key 
409036     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/charListRules.key 
409036     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExTheory.key 
409036     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExHeader.key 
409036     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExAxioms.key 
409051     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExLemmaProven.key 
409051     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqEq.key 
409051     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/infFlow.key 
409051     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/mapSize.key 
409051     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wd.key 
409067     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdHeader.key 
409067     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdGeneralRules.key 
409067     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdNumericalRules.key 
409083     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdLocSetRules.key 
409083     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdHeapRules.key 
409083     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdReachRules.key 
409083     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdSeqRules.key 
409083     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdStringRules.key 
409083     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdRegExRules.key 
409083     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdFormulaRules.key 
409098     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopInvariantRules.key 
409098     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/forLoopRules.key 
409098     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/execRules.key 
409129     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopScopeRules.key 
409146     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\gcd.key 
409989     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\A.java 
409989     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\Gcd.java 
409989     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 
409989     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
412003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 
412004     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\gcd.key 
425062     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
425912     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\A.java 
425912     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\Gcd.java 
425912     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 
425912     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
427892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 190.75ms 
427892     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
427892     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
428808     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\A.java 
428808     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\Gcd.java 
428823     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 
428823     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
430600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.5ns 
430600     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
437602     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
438563     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\A.java 
438563     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\Gcd.java 
438578     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 
438578     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
440774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 337.77ms 
440774     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
440774     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
441651     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\A.java 
441651     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\Gcd.java 
441667     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
444194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 621.27ms 
444194     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
444194     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
444960     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 
444960     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
446778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 271.3ns 
446778     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
446778     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
447670     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 
447670     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
449423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 183.9ns 
449423     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
449469     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
450352     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\A.java 
450352     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\Gcd.java 
450368     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
452941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 711.17ms 
452941     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
452956     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
453723     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 
453723     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
455498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 182.2ns 
455498     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
455513     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\gcd.mergePointStatements.key 
456432     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\A.java 
456432     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\Gcd.java 
456432     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 
456432     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
458230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ns 
458245     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\gcd.mergePointStatements.key 
465160     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\gcd.closed.proof 
466041     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\A.java 
466041     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\merge\Gcd.java 
466041     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
468276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 408.68ms 
468276     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\merge\gcd.closed.proof