TestCE

12

tests

0

failures

0

ignored

16.885s

duration

100%

successful

Tests

Test Duration Result
testMiddle() 16.239s passed
testOverFlow1() 0.586s passed
testOverFlow2() 0.004s passed
testTypes1() 0.002s passed
testTypes2() 0.001s passed
testTypes3() 0.001s passed
testTypes4() 0.003s passed
testTypes5() 0.001s passed
testTypes6() 0.002s passed
testTypes7() 0.045s passed
testTypes8() 0.001s passed
testTypes9() 0s passed

Standard output

23:46:03,076 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
23:46:03,123 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
23:46:03,139 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/D:/a/key/key/key.core.testgen/build/resources/test/logback.xml]
23:46:03,421 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
23:46:03,421 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
23:46:03,452 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
23:46:03,452 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
23:46:03,452 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
23:46:03,483 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to DEBUG
23:46:03,499 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
23:46:03,499 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@5ae81e1 - End of configuration.
23:46:03,499 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@2fd1731c - Registering current configuration as safe fallback point

1392       WARN  Test worker     d.u.i.k.t.s.c.TestCE      Warning: Z3_CE is not installed, tests skipped. 
1392       WARN  Test worker     d.u.i.k.t.s.c.TestCE      Maybe use JVM system property "z3SolverPath" to define the path to the Z3 command. 
1501       WARN  Test worker     d.u.i.k.s.ProofIndependentSettings The settings in C:\Users\runneradmin\.key\proofIndependentSettings.props are *not* read due to flag 'key.disregardSettings' 
1532       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\smt\ce\middle.key 
2064       WARN  Test worker     d.u.i.k.s.ProofSettings   The settings in C:\Users\runneradmin\.key\proof-settings.props are *not* read. 
2064       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/standardRules.key 
2314       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ldt.key 
2345       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/boolean.key 
2377       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key 
2455       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/integerHeader.key 
2471       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/floatHeader.key 
2486       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/heap.key 
2486       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/locSets.key 
2486       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/permission.key 
2502       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/reach.key 
2502       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/seq.key 
2502       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/map.key 
2596       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/freeADT.key 
2611       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/wellfound.key 
2611       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/charListHeader.key 
2877       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/propRule.key 
2987       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/firstOrderRules.key 
3033       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/ifThenElseRules.key 
3096       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/formulaNormalisationRules.key 
3283       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/updateRules.key 
3314       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/integerRulesCommon.key 
3521       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/intRules.key 
3583       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/intRulesUncheckedSemantics.key 
3646       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/intRulesCheckedSemantics.key 
3646       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/intRulesJavaSemantics.key 
3661       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/integerSimplificationRules.key 
4068       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4068       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4068       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4068       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4114       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/intDiv.key 
4177       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/bsum.key 
4427       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/bprod.key 
4474       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/binaryAxioms.key 
4490       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/binaryLemmas.key 
4506       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/intPow.key 
4615       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/floatRulesCommon.key 
4662       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/floatRules.key 
4662       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/floatRulesVerifyNormal.key 
4662       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/floatRulesAssumeStrictfp.key 
4724       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/genericRules.key 
4771       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/booleanRules.key 
4771       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/epsilon.key 
4787       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/locSetsRules.key 
4881       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/heapRules.key 
5037       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/permissionRules.key 
5068       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/reachRules.key 
5115       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/seqCoreRules.key 
5131       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/seqRules.key 
5209       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/seqPerm.key 
5256       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/seqPerm2.key 
5256       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/javaRules.key 
5428       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/assertions.key 
6397       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/loopRules.key 
6413       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/activeUse.key 
6512       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/instanceAllocation.key 
6558       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/java5.key 
6558       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/integerAssignment2UpdateRules.key 
6621       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/floatAssignment2UpdateRules.key 
6652       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/bigint.key 
6683       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
6683       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/adtProgramDecompositionRules.key 
6715       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/precRules.key 
6715       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/charListRules.key 
6746       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/regExTheory.key 
6746       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/regExHeader.key 
6746       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/regExAxioms.key 
6762       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/regExLemmaProven.key 
6777       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/seqEq.key 
6777       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/infFlow.key 
6793       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/mapSize.key 
6809       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/wd.key 
6824       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/wdHeader.key 
6824       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/wdGeneralRules.key 
6840       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/wdNumericalRules.key 
6887       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/wdLocSetRules.key 
6887       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/wdHeapRules.key 
6902       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/wdReachRules.key 
6902       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/wdSeqRules.key 
6902       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/wdStringRules.key 
6918       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/wdRegExRules.key 
6918       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/wdFormulaRules.key 
6949       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/loopInvariantRules.key 
6949       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/forLoopRules.key 
6965       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/execRules.key 
7121       DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/proof/rules/loopScopeRules.key 
10701      DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core.testgen\src\test\resources\testcase\smt\ce\src\Middle.java 
10717      DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core.testgen\src\test\resources\testcase\smt\ce\src\Test.java 
10764      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 
10795      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file jar:file:/D:/a/key/key/key.core/build/libs/key.core-2.11.0.jar!/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
14532      DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file src\test\resources\testcase\smt\ce\middle.key