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.799s | 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.809s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.808s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.812s | 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.798s | 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.793s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.818s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.834s | 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.811s | 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.826s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.913s | 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.817s | 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.804s | 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.813s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.879s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.796s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.836s | 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.886s | 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.921s | 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.862s | 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.847s | 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.824s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.818s | 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.819s | 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.791s | passed |
Standard output
664089 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 664089 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 664089 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.9ns 664092 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 666875 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 666875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 666890 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 667000 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_15715454961786302064.key 667000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_15715454961786302064.key 667000 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.2ns 667000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 669752 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 669767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_15715454961786302064.key 669767 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 669879 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 669879 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 669879 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.8ns 669879 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 672643 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 672659 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 672690 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.02ms 672800 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_13199122041693715570.key 672800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_13199122041693715570.key 672800 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.1ns 672800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 675534 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 675550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_13199122041693715570.key 675550 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 247.7ns 675663 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_1505999990808422256.key 675663 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_1505999990808422256.key 675663 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.2ns 675663 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 678386 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 678401 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_1505999990808422256.key 678401 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 678511 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_2942191910383561829.key 678511 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_2942191910383561829.key 678511 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.3ns 678511 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 681208 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 681224 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_2942191910383561829.key 681224 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 681335 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17828744175514859233.key 681335 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17828744175514859233.key 681335 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.8ns 681335 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 684029 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 684044 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_17828744175514859233.key 684044 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 684154 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_841136829420371722.key 684154 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_841136829420371722.key 684154 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249ns 684154 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 686847 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 686863 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_841136829420371722.key 686863 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 686972 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_7545968232190379812.key 686972 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_7545968232190379812.key 686972 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.4ns 686972 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 689639 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 689639 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_7545968232190379812.key 689655 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 689764 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_10750539609629216338.key 689764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_10750539609629216338.key 689764 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.9ns 689764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 692437 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 692453 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_10750539609629216338.key 692453 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 692563 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 692563 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 692563 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.8ns 692563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 695244 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 695260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 695260 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 695373 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_2405042775885418501.key 695373 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_2405042775885418501.key 695373 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.9ns 695373 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 698050 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 698065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_2405042775885418501.key 698065 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 698181 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_9869108518028156924.key 698181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_9869108518028156924.key 698181 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.7ns 698181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 700863 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 700879 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_9869108518028156924.key 700879 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 700994 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_6758715460735645109.key 700994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_6758715460735645109.key 700994 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.6ns 700994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 703667 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 703683 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_6758715460735645109.key 703683 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 703792 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11034640002491118162.key 703792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11034640002491118162.key 703792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.7ns 703792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 706460 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 706476 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_11034640002491118162.key 706476 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 706586 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9418812945148854867.key 706586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9418812945148854867.key 706586 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.4ns 706586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 709276 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 709292 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_9418812945148854867.key 709292 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 709404 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_18349209542279928558.key 709404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_18349209542279928558.key 709404 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.5ns 709404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 712110 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 712126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_18349209542279928558.key 712126 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 712239 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_6499134451788609377.key 712239 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_6499134451788609377.key 712239 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.4ns 712239 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 714924 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 714940 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_6499134451788609377.key 714940 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.1ns 715049 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6547509349870056595.key 715049 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6547509349870056595.key 715049 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.3ns 715049 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 717748 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 717763 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_6547509349870056595.key 717763 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 717875 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_2069502499858763335.key 717875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_2069502499858763335.key 717875 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.1ns 717875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 720561 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 720577 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_2069502499858763335.key 720577 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 720693 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_17502725913877969975.key 720693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_17502725913877969975.key 720693 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.1ns 720693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 723365 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 723381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_17502725913877969975.key 723381 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 723497 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_5300467205266279934.key 723497 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_5300467205266279934.key 723497 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.4ns 723497 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 726182 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 726198 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_5300467205266279934.key 726198 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 726311 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_9525418639975962685.key 726311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_9525418639975962685.key 726311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.9ns 726311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 729061 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 729076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_9525418639975962685.key 729076 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 729191 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_8263371468468298103.key 729191 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_8263371468468298103.key 729191 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.9ns 729191 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 731861 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 731877 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_8263371468468298103.key 731877 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 731987 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12702151029723013207.key 731987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12702151029723013207.key 731987 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.6ns 731987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 734696 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 734712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_12702151029723013207.key 734712 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns