ProveSMTLemmasTest
|
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.646s | 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.614s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.640s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.626s | 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.590s | 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.581s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.630s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.613s | 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.563s | 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.574s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.666s | 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.607s | 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.584s | 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.571s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.571s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.558s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.617s | 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.672s | 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.709s | 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.778s | 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.645s | 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.653s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.627s | 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.711s | 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.625s | passed |
Standard output
612676 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 612676 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 612676 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 612676 WARN Test worker d.u.i.k.n.ParsingFacade D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof took 0 ms to parse. 612676 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 612676 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 613447 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. 613447 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 615213 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 615230 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 615230 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 615230 WARN Test worker d.u.i.k.n.ParsingFacade D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof took 0 ms to parse. 615230 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 615342 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_4024744780974953822.key 615342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_4024744780974953822.key 615342 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 209ns 615342 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_4024744780974953822.key took 0 ms to parse. 615342 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 615342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 616105 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. 616105 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 617871 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 617887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_4024744780974953822.key 617887 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 617887 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_4024744780974953822.key took 0 ms to parse. 617887 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 618003 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 618003 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 618003 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.9ns 618003 WARN Test worker d.u.i.k.n.ParsingFacade D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof took 0 ms to parse. 618003 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 618003 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 618910 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. 618910 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 620567 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 620582 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 620598 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.18ms 620598 WARN Test worker d.u.i.k.n.ParsingFacade D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof took 0 ms to parse. 620598 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 620713 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3013939859213506905.key 620713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3013939859213506905.key 620713 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.1ns 620713 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3013939859213506905.key took 0 ms to parse. 620713 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 620713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 621614 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. 621614 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 623349 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 623364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_3013939859213506905.key 623374 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.2ns 623375 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3013939859213506905.key took 0 ms to parse. 623375 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 623490 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_3104898450783107745.key 623490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_3104898450783107745.key 623490 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.2ns 623490 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_3104898450783107745.key took 0 ms to parse. 623490 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 623490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 624271 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. 624271 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 626008 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 626023 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_3104898450783107745.key 626023 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 626023 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_3104898450783107745.key took 0 ms to parse. 626023 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 626135 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_4293693518824342733.key 626135 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_4293693518824342733.key 626135 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.6ns 626135 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_4293693518824342733.key took 0 ms to parse. 626135 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 626135 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 626917 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. 626917 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 628657 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 628673 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_4293693518824342733.key 628673 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 628673 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_4293693518824342733.key took 0 ms to parse. 628673 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 628788 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8300367215725732722.key 628788 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8300367215725732722.key 628788 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.8ns 628788 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8300367215725732722.key took 0 ms to parse. 628788 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1885 ms. 628788 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 629663 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 16 ms to parse. 629663 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 631290 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 631306 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_8300367215725732722.key 631306 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 631306 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8300367215725732722.key took 0 ms to parse. 631306 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 631416 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_53056668721042029.key 631416 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_53056668721042029.key 631416 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.3ns 631416 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_53056668721042029.key took 0 ms to parse. 631416 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 631416 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 632276 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. 632276 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 633996 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 634012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_53056668721042029.key 634012 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 634012 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_53056668721042029.key took 0 ms to parse. 634012 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 634127 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_14167855002597607700.key 634127 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_14167855002597607700.key 634127 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.4ns 634127 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_14167855002597607700.key took 0 ms to parse. 634127 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 634127 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 634932 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. 634932 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 636628 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 636644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_14167855002597607700.key 636644 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 636644 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_14167855002597607700.key took 0 ms to parse. 636644 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 636753 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6098474431882044956.key 636753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6098474431882044956.key 636753 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.8ns 636753 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6098474431882044956.key took 0 ms to parse. 636753 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 636753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 637554 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. 637554 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 639274 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 639290 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_6098474431882044956.key 639290 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 639290 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6098474431882044956.key took 0 ms to parse. 639290 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 639399 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 639399 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 639399 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.1ns 639399 WARN Test worker d.u.i.k.n.ParsingFacade D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof took 0 ms to parse. 639399 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 639399 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 640243 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. 640243 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 641885 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 641901 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 641901 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 641901 WARN Test worker d.u.i.k.n.ParsingFacade D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof took 0 ms to parse. 641901 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 642013 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11620733892072518586.key 642013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11620733892072518586.key 642013 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.7ns 642013 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11620733892072518586.key took 0 ms to parse. 642013 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 642013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 642848 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. 642848 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 644525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 644539 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_11620733892072518586.key 644539 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 644539 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11620733892072518586.key took 0 ms to parse. 644539 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 644653 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_14270988800530090323.key 644653 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_14270988800530090323.key 644653 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.1ns 644653 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_14270988800530090323.key took 0 ms to parse. 644653 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 644653 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 645451 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. 645451 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 647155 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 647155 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_14270988800530090323.key 647171 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 647171 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_14270988800530090323.key took 0 ms to parse. 647171 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 647280 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_28128878432901634.key 647280 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_28128878432901634.key 647280 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.8ns 647280 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_28128878432901634.key took 0 ms to parse. 647280 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 647280 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 648062 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. 648062 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 649739 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 649754 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_28128878432901634.key 649754 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 649754 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_28128878432901634.key took 0 ms to parse. 649754 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 649870 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12150628995538083257.key 649870 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12150628995538083257.key 649870 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 276ns 649870 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12150628995538083257.key took 0 ms to parse. 649870 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 649870 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 650636 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. 650636 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 652324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 652340 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_12150628995538083257.key 652340 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 652340 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12150628995538083257.key took 0 ms to parse. 652340 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 652451 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4631855762603659830.key 652451 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4631855762603659830.key 652451 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.6ns 652451 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4631855762603659830.key took 0 ms to parse. 652451 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 652451 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 653290 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. 653290 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 654957 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 654972 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_4631855762603659830.key 654972 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 654972 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4631855762603659830.key took 0 ms to parse. 654972 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 655082 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_12679416121386012448.key 655082 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_12679416121386012448.key 655082 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.9ns 655082 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_12679416121386012448.key took 0 ms to parse. 655082 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 655082 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 655864 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. 655864 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 657568 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 657584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_12679416121386012448.key 657584 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.2ns 657584 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_12679416121386012448.key took 0 ms to parse. 657584 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 657695 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_8842006941420805850.key 657695 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_8842006941420805850.key 657695 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.1ns 657695 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_8842006941420805850.key took 0 ms to parse. 657695 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 657695 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 658461 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. 658461 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 660126 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 660142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_8842006941420805850.key 660142 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 660142 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_8842006941420805850.key took 0 ms to parse. 660142 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 660258 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_9360596430073816523.key 660258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_9360596430073816523.key 660258 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.6ns 660258 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_9360596430073816523.key took 0 ms to parse. 660258 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 660258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 661029 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. 661029 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 662702 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 662718 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_9360596430073816523.key 662718 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 662718 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_9360596430073816523.key took 0 ms to parse. 662718 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 662833 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_17507314295850876918.key 662833 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_17507314295850876918.key 662833 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.7ns 662833 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_17507314295850876918.key took 0 ms to parse. 662833 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 662833 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 663645 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. 663645 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 665312 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 665312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_17507314295850876918.key 665328 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 665328 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_17507314295850876918.key took 0 ms to parse. 665328 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 665440 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5877774994122610600.key 665440 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5877774994122610600.key 665440 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.2ns 665440 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5877774994122610600.key took 0 ms to parse. 665440 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 665440 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 666222 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. 666222 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 667884 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 667900 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_5877774994122610600.key 667900 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 667900 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5877774994122610600.key took 0 ms to parse. 667916 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 668025 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_4492019971272455047.key 668025 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_4492019971272455047.key 668025 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.7ns 668025 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_4492019971272455047.key took 0 ms to parse. 668025 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 668025 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 668791 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. 668791 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 670471 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 670487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_4492019971272455047.key 670487 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 670487 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_4492019971272455047.key took 0 ms to parse. 670487 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 670596 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_5453281664041950024.key 670596 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_5453281664041950024.key 670596 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 416.8ns 670596 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_5453281664041950024.key took 0 ms to parse. 670596 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 670596 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 671363 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. 671363 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 673038 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 673053 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_5453281664041950024.key 673053 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 673053 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_5453281664041950024.key took 0 ms to parse. 673053 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 673168 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_14257890844221778343.key 673168 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_14257890844221778343.key 673168 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.5ns 673168 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_14257890844221778343.key took 0 ms to parse. 673168 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 673168 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 673975 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. 673975 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 675601 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 675616 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_14257890844221778343.key 675616 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 675616 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_14257890844221778343.key took 0 ms to parse. 675616 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 675726 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_4347099003929955990.key 675726 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_4347099003929955990.key 675726 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.2ns 675726 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_4347099003929955990.key took 0 ms to parse. 675726 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 675726 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 676539 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. 676539 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms. 678219 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 678234 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_4347099003929955990.key 678234 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 678234 WARN Test worker d.u.i.k.n.ParsingFacade C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_4347099003929955990.key took 0 ms to parse. 678234 WARN Test worker d.u.i.k.n.ParsingFacade Parsing time 1901 ms.