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.780s | 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.726s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.738s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.710s | 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.757s | 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.763s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.785s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.756s | 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.795s | 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.774s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.809s | 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.796s | 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.776s | 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.790s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.799s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.792s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.817s | 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.881s | 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.814s | 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.829s | 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.842s | 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.783s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.721s | 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.768s | 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.752s | passed |
Standard output
620728 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 620744 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 620744 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 620744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 623426 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 623442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 623442 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 623551 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_9720985425219490193.key 623551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_9720985425219490193.key 623551 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.5ns 623551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 626293 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 626308 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_9720985425219490193.key 626308 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 626421 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 626421 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 626421 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.9ns 626421 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 629087 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 629102 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 629118 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.61ms 629236 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_14877894760898532897.key 629236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_14877894760898532897.key 629236 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.3ns 629236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 631940 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 631940 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_14877894760898532897.key 631956 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 632065 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_13257835065033597262.key 632065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_13257835065033597262.key 632065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 289ns 632065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 634701 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 634716 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_13257835065033597262.key 634716 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 634904 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7392953249118982336.key 634904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7392953249118982336.key 634904 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.1ns 634904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 637565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 637581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_7392953249118982336.key 637581 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 637690 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6116803534258515398.key 637690 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6116803534258515398.key 637690 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.1ns 637690 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 640296 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 640296 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_6116803534258515398.key 640296 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 640412 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15667244827717727390.key 640412 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15667244827717727390.key 640412 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.9ns 640412 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 643064 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 643064 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_15667244827717727390.key 643064 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 643179 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_17087574944149859597.key 643179 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_17087574944149859597.key 643179 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.8ns 643179 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 645807 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 645823 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_17087574944149859597.key 645823 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 645932 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_18298785507395670152.key 645932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_18298785507395670152.key 645932 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.2ns 645932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 648586 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 648601 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_18298785507395670152.key 648601 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 648712 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 648712 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 648712 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.2ns 648712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 651313 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 651329 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 651329 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 651439 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14223056478463824851.key 651439 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14223056478463824851.key 651439 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 184ns 651439 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 654060 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 654060 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_14223056478463824851.key 654060 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 654177 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13276677158772454313.key 654177 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13276677158772454313.key 654177 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.3ns 654177 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 656760 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 656776 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_13276677158772454313.key 656776 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 656887 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9714134992952894395.key 656887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9714134992952894395.key 656887 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.6ns 656887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 659516 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 659531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_9714134992952894395.key 659531 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 659644 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_18173553748473372694.key 659644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_18173553748473372694.key 659644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.7ns 659644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 662291 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 662291 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_18173553748473372694.key 662291 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 662407 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16838231771995643.key 662407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16838231771995643.key 662407 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.6ns 662407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 665067 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 665083 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_16838231771995643.key 665083 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 665193 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_10483435385316284083.key 665193 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_10483435385316284083.key 665193 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.4ns 665193 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 667821 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 667837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_10483435385316284083.key 667837 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 667949 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_17019964883509295016.key 667949 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_17019964883509295016.key 667949 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.8ns 667949 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 670619 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 670634 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_17019964883509295016.key 670634 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 670744 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2570775443512197705.key 670744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2570775443512197705.key 670744 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.3ns 670744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 673393 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 673409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_2570775443512197705.key 673409 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 673518 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_17011537281444844518.key 673518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_17011537281444844518.key 673518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.7ns 673518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 676185 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 676201 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_17011537281444844518.key 676201 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 676314 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_8275573890206816026.key 676314 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_8275573890206816026.key 676314 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.3ns 676314 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 678966 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 678982 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_8275573890206816026.key 678982 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 679091 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_3079645182670664059.key 679091 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_3079645182670664059.key 679091 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.5ns 679091 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 681755 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 681771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_3079645182670664059.key 681771 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 681881 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15853285076461050495.key 681881 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15853285076461050495.key 681881 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.8ns 681881 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 684555 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 684555 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_15853285076461050495.key 684571 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 684681 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_3429870814094783127.key 684681 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_3429870814094783127.key 684681 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.1ns 684681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 687348 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 687363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_3429870814094783127.key 687363 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 687473 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_5105416940071324947.key 687473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_5105416940071324947.key 687473 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.4ns 687473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 690165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 690180 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_5105416940071324947.key 690180 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns