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.816s | 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.798s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.815s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.835s | 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.825s | 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.782s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.793s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.775s | 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.809s | 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.748s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.893s | 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.767s | 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.768s | 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.775s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.781s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.799s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.763s | 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.874s | 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.918s | 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.857s | 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.899s | 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.847s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.783s | 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.832s | 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.807s | passed |
Standard output
669294 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 669294 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 669294 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.6ns 669294 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 672062 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 672078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 672078 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 672193 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_6058266942443905251.key 672193 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_6058266942443905251.key 672193 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.5ns 672193 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 674943 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 674959 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_6058266942443905251.key 674959 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 675068 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 675068 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 675068 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.5ns 675068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 677831 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 677846 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 677878 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.16ms 677987 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_2777527987479838523.key 677987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_2777527987479838523.key 677987 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.2ns 677987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 680703 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 680719 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_2777527987479838523.key 680719 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 680844 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_16357593584685706773.key 680844 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_16357593584685706773.key 680844 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.5ns 680844 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 683616 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 683631 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_16357593584685706773.key 683631 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 683746 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_6256502342209919501.key 683746 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_6256502342209919501.key 683746 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.3ns 683746 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 686462 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 686477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_6256502342209919501.key 686477 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 686590 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_1796591457246814247.key 686590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_1796591457246814247.key 686590 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.1ns 686590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 689249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 689264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_1796591457246814247.key 689264 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ns 689374 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4387368131932178484.key 689374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4387368131932178484.key 689374 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.8ns 689374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 692080 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 692096 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_4387368131932178484.key 692096 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ns 692206 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_3057558613176640695.key 692206 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_3057558613176640695.key 692206 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.1ns 692206 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 694887 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 694903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_3057558613176640695.key 694903 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 695013 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_8851126026107852578.key 695013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_8851126026107852578.key 695013 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.6ns 695013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 697705 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 697721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_8851126026107852578.key 697721 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 697830 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 697830 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 697830 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.4ns 697830 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 700503 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 700519 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 700519 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 700628 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_13257993710522680267.key 700628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_13257993710522680267.key 700628 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.4ns 700628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 703319 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 703319 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_13257993710522680267.key 703334 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 703444 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11878820887217620727.key 703444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11878820887217620727.key 703444 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.8ns 703444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 706149 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 706164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_11878820887217620727.key 706164 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ns 706280 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17760733135578760388.key 706280 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17760733135578760388.key 706280 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.8ns 706280 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 708964 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 708980 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_17760733135578760388.key 708996 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 709105 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_16039741987041566613.key 709105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_16039741987041566613.key 709105 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 329ns 709105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 711760 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 711775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_16039741987041566613.key 711775 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 711889 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10554199934181899404.key 711889 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10554199934181899404.key 711889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243ns 711889 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 714556 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 714556 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_10554199934181899404.key 714572 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 714682 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_12505068820850215496.key 714682 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_12505068820850215496.key 714682 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 215ns 714682 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 717332 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 717347 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_12505068820850215496.key 717347 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 717457 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15843259856531099634.key 717457 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15843259856531099634.key 717457 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213ns 717457 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 720125 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 720141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_15843259856531099634.key 720141 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 720266 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8953236534189013218.key 720266 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8953236534189013218.key 720266 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 771.2ns 720266 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 722887 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 722903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_8953236534189013218.key 722903 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ns 723014 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_2281428619785286185.key 723014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_2281428619785286185.key 723014 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.6ns 723014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 725656 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 725671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_2281428619785286185.key 725671 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 725781 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14911263294198176474.key 725781 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14911263294198176474.key 725781 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.3ns 725781 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 728420 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 728436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_14911263294198176474.key 728436 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ns 728549 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_4906598045946785082.key 728549 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_4906598045946785082.key 728549 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.1ns 728549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 731194 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 731209 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_4906598045946785082.key 731209 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 731325 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_4106535862184307009.key 731325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_4106535862184307009.key 731325 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.1ns 731325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 733981 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 733981 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_4106535862184307009.key 733996 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 734106 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_14882052631030958248.key 734106 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_14882052631030958248.key 734106 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.1ns 734106 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 736780 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 736795 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_14882052631030958248.key 736795 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ns 736906 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6380260947965674020.key 736906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6380260947965674020.key 736906 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.7ns 736906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 739544 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 739560 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_6380260947965674020.key 739560 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns