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] | 3.454s | passed |
| [11] jdiv.dl, \forall int divNum; \forall int divDenom; jdiv(divNum,divDenom) = \if (divNum >= 0) \then (div(divNum,divDenom)) \else (div(divNum*(-1),divDenom)*(-1)) | testSMTLemmaSoundness(String, String)[11] | 3.282s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.257s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.309s | passed |
| [14] arrayRange.dl, \forall Object o; \forall Object o2; \forall Field f; \forall int lo; \forall int hi; (elementOf(o,f, arrayRange(o2, lo, hi))<<Trigger>> <-> o = o2 & \exists int iv; (f = arr(iv) & lo <= iv & iv <= hi)) | testSMTLemmaSoundness(String, String)[14] | 3.423s | passed |
| [15] seqConcat.dl, \forall int i; \forall Seq s1; \forall Seq s2; ( 0 <= i & i < seqLen(s1) + seqLen(s2) -> any::seqGet(seqConcat(s1, s2), i) = \if (i < seqLen(s1)) \then (any::seqGet(s1, i)) \else (any::seqGet(s2, i-seqLen(s1)))) | testSMTLemmaSoundness(String, String)[15] | 3.491s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.350s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.431s | passed |
| [18] freshLocs.dl, \forall Heap h; \forall Object o; \forall Field f; ( elementOf(o,f,freshLocs(h))<<Trigger>> <-> o != null & !boolean::select(h,o,java.lang.Object::<created>)=TRUE ) | testSMTLemmaSoundness(String, String)[18] | 3.384s | passed |
| [19] anon.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Heap h2; \forall LocSet ls; any::select(anon(h, ls, h2), o, f)<<Trigger>> = \if(elementOf(o, f, ls) & f != java.lang.Object::<created> | elementOf(o, f, freshLocs(h))) \then(any::select(h2, o, f)) \else(any::select(h, o, f)) | testSMTLemmaSoundness(String, String)[19] | 3.357s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.362s | passed |
| [20] memset.dl, \forall Heap h; \forall LocSet s; \forall any x; \forall Object o; \forall Field f; any::select(memset(h, s, x), o, f)<<Trigger>> = \if(elementOf(o, f, s) & f != java.lang.Object::<created>) \then(x) \else(any::select(h, o, f)) | testSMTLemmaSoundness(String, String)[20] | 3.252s | passed |
| [21] store.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; \forall any v; any::select(store(h,o,f,v), o2, f2)<<Trigger>> = \if(o = o2 & f = f2 & f != java.lang.Object::<created>) \then(v) \else(any::select(h, o2, f2)) | testSMTLemmaSoundness(String, String)[21] | 3.540s | passed |
| [22] seqSub.dl.2, \forall Seq seq; \forall int from; \forall int to; seqLen(seqSub(seq, from, to)<<Trigger>>) = \if(from < to)\then(to - from)\else(0) | testSMTLemmaSoundness(String, String)[22] | 3.404s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.380s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.371s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.255s | passed |
| [2] seqSub.dl, \forall Seq seq; \forall int from; \forall int to; \forall int idx; any::seqGet(seqSub(seq, from, to)<<Trigger>>, idx) = \if(0 <= idx & idx < (to - from)) \then(any::seqGet(seq, idx + from)) \else(seqGetOutside) | testSMTLemmaSoundness(String, String)[2] | 3.505s | passed |
| [3] seqGetOutside.dl, \forall int i; \forall Seq s; ( i < 0 | i >= seqLen(s) -> any::seqGet(s, i)<<Trigger>> = seqGetOutside ) | testSMTLemmaSoundness(String, String)[3] | 3.441s | passed |
| [4] singleton.dl, \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; ( elementOf(o,f, singleton(o2,f2))<<Trigger>> <-> o = o2 & f = f2 ) | testSMTLemmaSoundness(String, String)[4] | 3.527s | passed |
| [5] create.dl, \forall Heap h; \forall Object o; \forall Object o2; \forall Field f; any::select(create(h, o), o2, f)<<Trigger>> = \if(o = o2 & o != null & f = java.lang.Object::<created>) \then(TRUE) \else(any::select(h, o2, f)) | testSMTLemmaSoundness(String, String)[5] | 3.271s | passed |
| [6] allFields.dl, \forall Object o; \forall Field f; \forall Object o2; ( elementOf(o,f, allFields(o2))<<Trigger>> <-> o = o2 ) | testSMTLemmaSoundness(String, String)[6] | 3.287s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.315s | passed |
| [8] union.dl, \forall Object o; \forall Field f; \forall LocSet l1; \forall LocSet l2; ( elementOf(o, f, union(l1, l2))<<Trigger>> <-> elementOf(o,f,l1) | elementOf(o,f,l2) ) | testSMTLemmaSoundness(String, String)[8] | 3.422s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 3.444s | passed |
Standard output
794854 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 794854 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 794854 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns 794854 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 798061 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 798077 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 798077 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 798202 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8314471402446900461.key 798202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8314471402446900461.key 798202 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.9ns 798202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 801577 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 801595 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_8314471402446900461.key 801596 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 801707 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 801707 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 801707 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 801726 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 804992 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 805008 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 805023 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.32ms 805148 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_17446977602384740066.key 805148 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_17446977602384740066.key 805148 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.7ns 805148 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 808534 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 808550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_17446977602384740066.key 808550 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 808675 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17958301679508094114.key 808675 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17958301679508094114.key 808675 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.4ns 808675 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 811816 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 811831 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_17958301679508094114.key 811831 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 811946 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_712288357018953214.key 811946 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_712288357018953214.key 811946 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161ns 811946 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 815105 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 815120 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_712288357018953214.key 815120 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 815234 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_9402628195781319760.key 815234 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_9402628195781319760.key 815234 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.2ns 815234 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 818409 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 818440 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_9402628195781319760.key 818440 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 818549 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3769165686942570806.key 818549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3769165686942570806.key 818549 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.6ns 818549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 821836 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 821851 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_3769165686942570806.key 821867 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 821971 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_6050436821072754565.key 821971 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_6050436821072754565.key 821971 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.6ns 821971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 825290 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 825306 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_6050436821072754565.key 825306 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 825415 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6396929624147289784.key 825415 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6396929624147289784.key 825415 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.4ns 825415 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 828663 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 828759 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_6396929624147289784.key 828759 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 828869 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 828869 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 828869 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.9ns 828869 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 832011 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 832026 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 832042 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.44ms 832151 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_2833277713885801623.key 832151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_2833277713885801623.key 832151 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.6ns 832151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 835278 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 835294 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_2833277713885801623.key 835294 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 835408 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8259819369053185265.key 835408 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8259819369053185265.key 835408 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.4ns 835408 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 838587 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 838602 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_8259819369053185265.key 838602 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 838717 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_13219844609911984218.key 838717 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_13219844609911984218.key 838717 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.9ns 838717 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 841937 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 842004 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_13219844609911984218.key 842004 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 842140 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12875889815222695981.key 842156 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12875889815222695981.key 842156 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.1ns 842156 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 845507 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 845522 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_12875889815222695981.key 845522 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 845632 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14370598355723247745.key 845632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14370598355723247745.key 845632 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.7ns 845632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 848858 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 848874 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_14370598355723247745.key 848874 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 848983 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_3413674840151958419.key 848983 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_3413674840151958419.key 848983 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.9ns 848983 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 852287 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 852303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_3413674840151958419.key 852303 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 852414 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15973043498264560525.key 852414 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15973043498264560525.key 852414 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230ns 852414 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 855657 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 855673 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_15973043498264560525.key 855673 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 855798 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_11535372732574436318.key 855798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_11535372732574436318.key 855798 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.2ns 855798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 859025 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 859041 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_11535372732574436318.key 859041 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 859155 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_6055603742562516954.key 859155 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_6055603742562516954.key 859155 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.2ns 859155 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 862282 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 862297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_6055603742562516954.key 862297 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 862407 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_16057901415955813683.key 862407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_16057901415955813683.key 862407 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.8ns 862407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 865798 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 865829 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_16057901415955813683.key 865829 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 865947 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_1558678225440190360.key 865947 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_1558678225440190360.key 865947 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 392ns 865947 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 869222 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 869238 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_1558678225440190360.key 869238 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 869351 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6561049744672750279.key 869351 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6561049744672750279.key 869351 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.4ns 869351 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 872606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 872606 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_6561049744672750279.key 872622 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 872731 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_14090750282125721367.key 872731 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_14090750282125721367.key 872731 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.8ns 872731 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 875970 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 875986 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_14090750282125721367.key 875986 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 876102 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_8622622944309462271.key 876102 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_8622622944309462271.key 876102 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.9ns 876102 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 879229 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 879244 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_8622622944309462271.key 879244 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns