ProveSMTLemmasTest

all > de.uka.ilkd.key.smt.newsmt2 > ProveSMTLemmasTest
25

tests
0

failures
0

ignored
1m5.42s

duration
100%

successful

Tests

Test Method name Duration Result
[10] wellFormed.dl, \forall Heap h; \forall Object o; \forall Field f; (wellFormed(h) -> boolean::select(h, (java.lang.Object::select(h, o, f))<<Trigger>>, java.lang.Object::<created>) = TRUE | (java.lang.Object::select(h, o, f)) = null) testSMTLemmaSoundness(String, String)[10] 2.590s passed
[11] jdiv.dl, \forall int divNum; \forall int divDenom; jdiv(divNum,divDenom) = \if (divNum >= 0) \then (div(divNum,divDenom)) \else (div(divNum*(-1),divDenom)*(-1)) testSMTLemmaSoundness(String, String)[11] 2.591s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 2.585s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 2.593s passed
[14] arrayRange.dl, \forall Object o; \forall Object o2; \forall Field f; \forall int lo; \forall int hi; (elementOf(o,f, arrayRange(o2, lo, hi))<<Trigger>> <-> o = o2 & \exists int iv; (f = arr(iv) & lo <= iv & iv <= hi)) testSMTLemmaSoundness(String, String)[14] 2.588s passed
[15] seqConcat.dl, \forall int i; \forall Seq s1; \forall Seq s2; ( 0 <= i & i < seqLen(s1) + seqLen(s2) -> any::seqGet(seqConcat(s1, s2), i) = \if (i < seqLen(s1)) \then (any::seqGet(s1, i)) \else (any::seqGet(s2, i-seqLen(s1)))) testSMTLemmaSoundness(String, String)[15] 2.585s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 2.593s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 2.594s passed
[18] freshLocs.dl, \forall Heap h; \forall Object o; \forall Field f; ( elementOf(o,f,freshLocs(h))<<Trigger>> <-> o != null & !boolean::select(h,o,java.lang.Object::<created>)=TRUE ) testSMTLemmaSoundness(String, String)[18] 2.592s passed
[19] anon.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Heap h2; \forall LocSet ls; any::select(anon(h, ls, h2), o, f)<<Trigger>> = \if(elementOf(o, f, ls) & f != java.lang.Object::<created> | elementOf(o, f, freshLocs(h))) \then(any::select(h2, o, f)) \else(any::select(h, o, f)) testSMTLemmaSoundness(String, String)[19] 2.605s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 2.688s passed
[20] memset.dl, \forall Heap h; \forall LocSet s; \forall any x; \forall Object o; \forall Field f; any::select(memset(h, s, x), o, f)<<Trigger>> = \if(elementOf(o, f, s) & f != java.lang.Object::<created>) \then(x) \else(any::select(h, o, f)) testSMTLemmaSoundness(String, String)[20] 2.596s passed
[21] store.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; \forall any v; any::select(store(h,o,f,v), o2, f2)<<Trigger>> = \if(o = o2 & f = f2 & f != java.lang.Object::<created>) \then(v) \else(any::select(h, o2, f2)) testSMTLemmaSoundness(String, String)[21] 2.636s passed
[22] seqSub.dl.2, \forall Seq seq; \forall int from; \forall int to; seqLen(seqSub(seq, from, to)<<Trigger>>) = \if(from < to)\then(to - from)\else(0) testSMTLemmaSoundness(String, String)[22] 2.620s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 2.589s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 2.589s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 2.583s passed
[2] seqSub.dl, \forall Seq seq; \forall int from; \forall int to; \forall int idx; any::seqGet(seqSub(seq, from, to)<<Trigger>>, idx) = \if(0 <= idx & idx < (to - from)) \then(any::seqGet(seq, idx + from)) \else(seqGetOutside) testSMTLemmaSoundness(String, String)[2] 2.721s passed
[3] seqGetOutside.dl, \forall int i; \forall Seq s; ( i < 0 | i >= seqLen(s) -> any::seqGet(s, i)<<Trigger>> = seqGetOutside ) testSMTLemmaSoundness(String, String)[3] 2.747s passed
[4] singleton.dl, \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; ( elementOf(o,f, singleton(o2,f2))<<Trigger>> <-> o = o2 & f = f2 ) testSMTLemmaSoundness(String, String)[4] 2.620s passed
[5] create.dl, \forall Heap h; \forall Object o; \forall Object o2; \forall Field f; any::select(create(h, o), o2, f)<<Trigger>> = \if(o = o2 & o != null & f = java.lang.Object::<created>) \then(TRUE) \else(any::select(h, o2, f)) testSMTLemmaSoundness(String, String)[5] 2.729s passed
[6] allFields.dl, \forall Object o; \forall Field f; \forall Object o2; ( elementOf(o,f, allFields(o2))<<Trigger>> <-> o = o2 ) testSMTLemmaSoundness(String, String)[6] 2.587s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 2.600s passed
[8] union.dl, \forall Object o; \forall Field f; \forall LocSet l1; \forall LocSet l2; ( elementOf(o, f, union(l1, l2))<<Trigger>> <-> elementOf(o,f,l1) | elementOf(o,f,l2) ) testSMTLemmaSoundness(String, String)[8] 2.589s passed
[9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) testSMTLemmaSoundness(String, String)[9] 2.612s passed

Standard output

601074     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 
601074     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 
601894     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 
603637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
603653     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 
603762     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10969073567738898463.key 
603762     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10969073567738898463.key 
604580     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 
606367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 
606367     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10969073567738898463.key 
606477     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 
606477     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 
607338     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 
609114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.27ms 
609114     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 
609224     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7664139652597483611.key 
609224     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7664139652597483611.key 
610031     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 
611736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.2ns 
611736     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7664139652597483611.key 
611845     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_7635370323878331575.key 
611845     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_7635370323878331575.key 
612770     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 
614462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
614462     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_7635370323878331575.key 
614575     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10039521681013743253.key 
614575     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10039521681013743253.key 
615375     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 
617044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
617044     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10039521681013743253.key 
617161     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_15994179444335511082.key 
617161     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_15994179444335511082.key 
617954     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 
619648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
619648     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_15994179444335511082.key 
619761     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6561832066074756066.key 
619761     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6561832066074756066.key 
620559     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 
622226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.1ns 
622226     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6561832066074756066.key 
622351     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_5643107287736376669.key 
622351     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_5643107287736376669.key 
623151     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 
624854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 
624854     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_5643107287736376669.key 
624963     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13363281445082198195.key 
624963     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13363281445082198195.key 
625762     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 
627441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
627441     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13363281445082198195.key 
627554     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 
627554     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 
628358     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 
630030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 873.6ns 
630030     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 
630145     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5511780698828012498.key 
630145     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5511780698828012498.key 
630943     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 
632616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
632616     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5511780698828012498.key 
632746     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13787906346972555731.key 
632746     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13787906346972555731.key 
633537     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 
635210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ns 
635210     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13787906346972555731.key 
635325     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10216933988877481180.key 
635325     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10216933988877481180.key 
636124     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 
637803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ns 
637803     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10216933988877481180.key 
637913     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6399165928901840402.key 
637913     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6399165928901840402.key 
638711     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 
640384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 
640384     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6399165928901840402.key 
640498     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10154354978492452749.key 
640498     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10154354978492452749.key 
641264     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 
642967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
642967     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10154354978492452749.key 
643092     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_334079701042246217.key 
643092     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_334079701042246217.key 
643881     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 
645577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
645577     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_334079701042246217.key 
645686     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_615408232617111195.key 
645686     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_615408232617111195.key 
646472     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 
648165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
648165     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_615408232617111195.key 
648278     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4015646035056801804.key 
648278     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4015646035056801804.key 
649075     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 
650773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 
650773     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4015646035056801804.key 
650883     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13565707238908991965.key 
650883     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13565707238908991965.key 
651690     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 
653369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
653369     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13565707238908991965.key 
653479     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1128365364671843266.key 
653479     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1128365364671843266.key 
654308     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 
656006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ns 
656006     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1128365364671843266.key 
656115     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_14813114180146602008.key 
656115     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_14813114180146602008.key 
656912     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 
658625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
658625     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_14813114180146602008.key 
658735     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_432966058339289147.key 
658735     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_432966058339289147.key 
659532     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 
661208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
661208     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_432966058339289147.key 
661324     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_1656325355661515004.key 
661324     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_1656325355661515004.key 
662121     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 
663804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 
663804     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_1656325355661515004.key 
663914     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_18069456909140220165.key 
663914     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_18069456909140220165.key 
664711     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 
666381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 
666381     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_18069456909140220165.key