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.990s | 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] | 4.011s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.983s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.983s | 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.997s | 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.980s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.962s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.984s | 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.989s | 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.993s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.030s | 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.994s | 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.998s | 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.989s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.993s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.994s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.984s | 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.993s | 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.994s | 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] | 4.002s | 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] | 4.005s | 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.987s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.985s | 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.980s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 4.007s | passed |
Standard output
896255 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 896255 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 896255 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 89ns 896255 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 900157 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.9s 900173 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 900173 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.99ms 900282 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10247331926453169061.key 900282 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10247331926453169061.key 900282 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.5ns 900282 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 904148 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 904164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_10247331926453169061.key 904164 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 904275 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 904275 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 904275 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.9ns 904275 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 908128 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 908144 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 908160 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.44ms 908269 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_4378013640520125386.key 908269 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_4378013640520125386.key 908269 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.8ns 908269 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 912142 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 912157 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_4378013640520125386.key 912157 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 912271 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_18022202601716264099.key 912271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_18022202601716264099.key 912271 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.1ns 912271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 916151 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 916167 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_18022202601716264099.key 916167 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 916276 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8593894072011433895.key 916276 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8593894072011433895.key 916276 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.1ns 916276 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 920131 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 920147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_8593894072011433895.key 920147 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 920263 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_12253690853389592346.key 920263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_12253690853389592346.key 920263 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 202ns 920263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 924115 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 924131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_12253690853389592346.key 924131 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.6ns 924248 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6050236686011739696.key 924248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6050236686011739696.key 924248 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.8ns 924248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 928103 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 928119 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_6050236686011739696.key 928119 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 928228 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_4179570637433058271.key 928228 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_4179570637433058271.key 928228 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.9ns 928228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 932110 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 932126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_4179570637433058271.key 932126 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 932235 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13641414315402977291.key 932235 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13641414315402977291.key 932235 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.3ns 932235 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 936094 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 936110 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_13641414315402977291.key 936110 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 936225 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 936225 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 936225 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.5ns 936225 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 940104 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.89s 940120 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 940120 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 767.3ns 940236 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_21684555243621144.key 940236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_21684555243621144.key 940236 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.1ns 940236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 944089 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 944104 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_21684555243621144.key 944104 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 944219 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_4462607474860710463.key 944219 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_4462607474860710463.key 944219 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.6ns 944219 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 948077 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 948092 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_4462607474860710463.key 948092 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 948202 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14572158014392216366.key 948202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14572158014392216366.key 948202 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.9ns 948202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 952068 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 952084 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_14572158014392216366.key 952084 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 952199 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9872409000847550208.key 952199 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9872409000847550208.key 952199 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.5ns 952199 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 956052 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 956068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_9872409000847550208.key 956068 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 956179 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_11594364588660322115.key 956179 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_11594364588660322115.key 956179 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.7ns 956179 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 960016 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.84s 960032 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_11594364588660322115.key 960032 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 960141 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_11924366529228322192.key 960141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_11924366529228322192.key 960141 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.5ns 960141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 963996 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 964012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_11924366529228322192.key 964012 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 964125 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2048184712662300377.key 964125 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2048184712662300377.key 964125 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 293ns 964125 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 967982 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 967998 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_2048184712662300377.key 967998 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 968114 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_5071720977746573092.key 968114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_5071720977746573092.key 968114 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 200ns 968114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 971979 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 971995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_5071720977746573092.key 971995 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 972107 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4651513485087744610.key 972107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4651513485087744610.key 972107 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.8ns 972107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 975974 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 975989 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_4651513485087744610.key 975989 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 976101 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_15293808922995521826.key 976101 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_15293808922995521826.key 976101 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 187ns 976101 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 979974 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 979990 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_15293808922995521826.key 979990 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 980099 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_2066280797412864792.key 980099 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_2066280797412864792.key 980099 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.5ns 980099 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 983962 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 983978 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_2066280797412864792.key 983978 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 984088 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3297282084242070665.key 984088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3297282084242070665.key 984088 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.6ns 984088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 987951 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 987967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_3297282084242070665.key 987967 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 988081 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_7736458314699762263.key 988081 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_7736458314699762263.key 988081 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.8ns 988081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 991951 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 991967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_7736458314699762263.key 991967 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 992076 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_5464259455360369442.key 992076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_5464259455360369442.key 992076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 280ns 992076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 995936 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 995952 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_5464259455360369442.key 995952 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns