ContractLoadingTests

4

tests

0

failures

0

ignored

11.709s

duration

100%

successful

Tests

Test Duration Result
issues1658() 2.585s passed
specMathBigintMathTest() 3.778s passed
specMathJavaMathTest() 2.759s passed
sumAndMax() 2.587s passed

Standard output

689755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java 
689755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.2ns 
689755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689755     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/standardRules.key took 0 ms to parse. 
689755     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689755     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ldt.key took 0 ms to parse. 
689755     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/boolean.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerHeader.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatHeader.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/heap.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/locSets.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/permission.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/reach.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seq.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/map.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/freeADT.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wellfound.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/charListHeader.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/propRule.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/firstOrderRules.key took 0 ms to parse. 
689770     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689786     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/ifThenElseRules.key took 0 ms to parse. 
689786     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689786     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/formulaNormalisationRules.key took 0 ms to parse. 
689786     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689786     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/updateRules.key took 0 ms to parse. 
689786     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689802     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerRulesCommon.key took 0 ms to parse. 
689802     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689802     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRules.key took 0 ms to parse. 
689802     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689802     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key took 0 ms to parse. 
689802     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689802     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesCheckedSemantics.key took 0 ms to parse. 
689802     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1902 ms. 
689817     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intRulesJavaSemantics.key took 15 ms to parse. 
689817     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1917 ms. 
689834     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key took 17 ms to parse. 
689834     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1934 ms. 
689849     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
689849     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
689849     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
689849     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
689849     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intDiv.key took 0 ms to parse. 
689849     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1934 ms. 
689864     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bsum.key took 0 ms to parse. 
689864     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1934 ms. 
689880     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bprod.key took 0 ms to parse. 
689880     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1934 ms. 
689880     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/binaryAxioms.key took 0 ms to parse. 
689880     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1934 ms. 
689880     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/binaryLemmas.key took 0 ms to parse. 
689880     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1934 ms. 
689880     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/intPow.key took 0 ms to parse. 
689880     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1934 ms. 
689896     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesCommon.key took 16 ms to parse. 
689896     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1950 ms. 
689898     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRules.key took 0 ms to parse. 
689898     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1950 ms. 
689898     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesVerifyNormal.key took 0 ms to parse. 
689898     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1950 ms. 
689898     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatRulesAssumeStrictfp.key took 0 ms to parse. 
689898     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1950 ms. 
689898     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/genericRules.key took 0 ms to parse. 
689898     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1950 ms. 
689898     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/booleanRules.key took 0 ms to parse. 
689898     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1950 ms. 
689914     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/epsilon.key took 16 ms to parse. 
689914     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1966 ms. 
689914     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/locSetsRules.key took 0 ms to parse. 
689914     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1966 ms. 
689929     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/heapRules.key took 0 ms to parse. 
689929     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1966 ms. 
689945     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/permissionRules.key took 0 ms to parse. 
689945     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1966 ms. 
689945     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/reachRules.key took 0 ms to parse. 
689945     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1966 ms. 
689961     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqCoreRules.key took 0 ms to parse. 
689961     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1966 ms. 
689961     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqRules.key took 0 ms to parse. 
689961     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1966 ms. 
689976     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqPerm.key took 0 ms to parse. 
689976     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1966 ms. 
689976     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqPerm2.key took 0 ms to parse. 
689976     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1966 ms. 
690008     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/javaRules.key took 16 ms to parse. 
690008     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1982 ms. 
690008     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/assertions.key took 0 ms to parse. 
690008     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1982 ms. 
690133     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopRules.key took 0 ms to parse. 
690133     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1982 ms. 
690133     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/activeUse.key took 0 ms to parse. 
690133     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1982 ms. 
690148     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/instanceAllocation.key took 0 ms to parse. 
690148     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1982 ms. 
690164     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/java5.key took 0 ms to parse. 
690164     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1982 ms. 
690168     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key took 2 ms to parse. 
690168     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1984 ms. 
690181     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key took 0 ms to parse. 
690181     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1984 ms. 
690181     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/bigint.key took 0 ms to parse. 
690181     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1984 ms. 
690197     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
690197     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/adtProgramDecompositionRules.key took 0 ms to parse. 
690197     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1984 ms. 
690197     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/precRules.key took 0 ms to parse. 
690197     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 1984 ms. 
690213     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/charListRules.key took 16 ms to parse. 
690213     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690213     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExTheory.key took 0 ms to parse. 
690213     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690213     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExHeader.key took 0 ms to parse. 
690213     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690213     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExAxioms.key took 0 ms to parse. 
690213     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690213     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/regExLemmaProven.key took 0 ms to parse. 
690213     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690213     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/seqEq.key took 0 ms to parse. 
690213     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690228     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/infFlow.key took 0 ms to parse. 
690228     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690228     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/mapSize.key took 0 ms to parse. 
690228     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690228     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wd.key took 0 ms to parse. 
690228     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690228     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdHeader.key took 0 ms to parse. 
690228     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690228     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdGeneralRules.key took 0 ms to parse. 
690228     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690228     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdNumericalRules.key took 0 ms to parse. 
690228     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690244     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdLocSetRules.key took 0 ms to parse. 
690244     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690244     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdHeapRules.key took 0 ms to parse. 
690244     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690260     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdReachRules.key took 0 ms to parse. 
690260     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690261     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdSeqRules.key took 0 ms to parse. 
690261     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2000 ms. 
690264     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdStringRules.key took 1 ms to parse. 
690264     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2001 ms. 
690266     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdRegExRules.key took 0 ms to parse. 
690266     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2001 ms. 
690266     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/wdFormulaRules.key took 0 ms to parse. 
690266     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2001 ms. 
690266     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopInvariantRules.key took 0 ms to parse. 
690266     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2001 ms. 
690266     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/forLoopRules.key took 0 ms to parse. 
690266     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2001 ms. 
690281     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/execRules.key took 0 ms to parse. 
690281     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2001 ms. 
690353     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/proof/rules/loopScopeRules.key took 0 ms to parse. 
690353     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2001 ms. 
691606     DEBUG Test worker     d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods. 
691669     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 0 ms to parse. 
691669     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2001 ms. 
693517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.77s 
693517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java 
693533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.4ms 
693533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694399     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 0 ms to parse. 
694399     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2001 ms. 
696105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
696105     INFO  Test worker     d.u.i.k.s.n.ContractLoadingTests self.sumAndMax(a) catch(exc)
pre: (  \forall int i;
     (   (0 <= i & i < a.length)<<SC>> & inInt(i)
      -> 0 <= a[i])
 & ((self.<inv><<impl>> & (!a = null)<<impl>>)<<SC>>))<<SC>>
post:   (\forall int i;
     (   (0 <= i & i < a.length)<<SC>> & inInt(i)
      -> a[i] <= self.max)
& ((  (   a.length >  0
       -> \exists int i;
            ((  (0 <= i
              & i < a.length)<<SC>>
              & inInt(i)
              & self.max = a[i])<<SC>>))
    & ((  self.sum = bsum{int i;}(0, a.length, a[i])
        & ((  self.sum <= a.length * self.max
            & self.<inv><<impl>>)<<SC>>))<<SC>>))<<SC>>))<<SC>>
& (exc = null)<<impl>>
mod:      {(self, SumAndMax::$sum)}
\cup {(self, SumAndMax::$max)}
termination: diamond 
696105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java 
696105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.4ns 
696121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697001     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 0 ms to parse. 
697001     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2001 ms. 
698690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
698690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java 
698690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.1ns 
698690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699581     DEBUG Test worker     d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods. 
699628     WARN  Test worker     d.u.i.k.n.ParsingFacade   file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key took 0 ms to parse. 
699628     WARN  Test worker     d.u.i.k.n.ParsingFacade   Parsing time 2001 ms. 
701442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s