ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m28.68s

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] 3.708s 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] 3.462s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 3.476s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 3.425s 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] 3.697s 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] 3.501s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 3.565s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 3.472s 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] 3.415s 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] 3.434s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 3.489s 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] 3.603s 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] 3.676s 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] 3.562s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 3.371s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 3.496s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 3.486s 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] 3.930s 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] 3.660s 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] 3.471s 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] 3.498s 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] 3.495s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 3.423s 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] 3.445s passed
[9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) testSMTLemmaSoundness(String, String)[9] 3.922s passed

Standard output

835766     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 
835766     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 
836860     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 
839127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.67ms 
839127     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 
839244     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10360625257161420062.key 
839244     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10360625257161420062.key 
840275     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 
842702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 
842702     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10360625257161420062.key 
843187     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 
843188     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 
844326     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 
846719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.23ms 
846719     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 
846835     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_1246183165256759688.key 
846835     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_1246183165256759688.key 
847867     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 
850191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
850191     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_1246183165256759688.key 
850306     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_7647489750348779531.key 
850306     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_7647489750348779531.key 
851484     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 
853694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 
853694     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_7647489750348779531.key 
853804     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7320174970181885665.key 
853804     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7320174970181885665.key 
854919     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 
857189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 
857189     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7320174970181885665.key 
857299     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_5319641331895381542.key 
857299     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_5319641331895381542.key 
858347     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 
860607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 
860607     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_5319641331895381542.key 
860722     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15521448683535603367.key 
860722     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15521448683535603367.key 
861769     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 
864053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 
864053     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15521448683535603367.key 
864167     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_5861031524087694663.key 
864167     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_5861031524087694663.key 
865277     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 
867715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
867715     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_5861031524087694663.key 
868117     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4342628074791182430.key 
868117     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4342628074791182430.key 
869407     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 
871704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
871704     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4342628074791182430.key 
871813     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 
871813     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 
872923     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 
875165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
875165     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 
875275     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3085785827538942479.key 
875275     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3085785827538942479.key 
876327     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 
878640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.8ns 
878640     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3085785827538942479.key 
878751     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_1215129964749003620.key 
878751     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_1215129964749003620.key 
879769     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 
882067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
882067     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_1215129964749003620.key 
882176     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17920713903042696384.key 
882176     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17920713903042696384.key 
883289     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 
885763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 
885763     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17920713903042696384.key 
885874     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15727494766472398943.key 
885874     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15727494766472398943.key 
887030     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 
889266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
889266     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15727494766472398943.key 
889376     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_7756641745666142581.key 
889376     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_7756641745666142581.key 
890424     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 
892831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 
892831     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_7756641745666142581.key 
892941     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_376974220602522756.key 
892941     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_376974220602522756.key 
894004     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 
896304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 
896304     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_376974220602522756.key 
896413     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18188612269875373524.key 
896413     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18188612269875373524.key 
897461     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 
899714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 
899714     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18188612269875373524.key 
899828     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2918760374797632253.key 
899828     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2918760374797632253.key 
900868     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 
903150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
903150     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2918760374797632253.key 
903262     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_9563286859109095165.key 
903262     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_9563286859109095165.key 
904340     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 
906748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 
906748     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_9563286859109095165.key 
906873     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14472378676427159974.key 
906873     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14472378676427159974.key 
908061     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 
910439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
910439     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14472378676427159974.key 
910553     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_7489588339993037459.key 
910553     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_7489588339993037459.key 
911584     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 
913999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 
913999     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_7489588339993037459.key 
914115     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_13808987009813312747.key 
914115     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_13808987009813312747.key 
915172     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 
917361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 
917361     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_13808987009813312747.key 
917486     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_17950319464273851045.key 
917486     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_17950319464273851045.key 
918571     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 
920872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 
920872     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_17950319464273851045.key 
920982     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_1220577181005252726.key 
920982     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_1220577181005252726.key 
922076     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 
924343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 
924343     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_1220577181005252726.key