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] | 5.677s | 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] | 5.660s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.597s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.488s | 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] | 5.582s | 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] | 5.677s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.628s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.581s | 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] | 5.566s | 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] | 5.566s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.524s | 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] | 5.629s | 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] | 5.614s | 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] | 5.752s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.566s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.597s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.630s | 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] | 5.503s | 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] | 5.455s | 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] | 5.567s | 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] | 5.613s | 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] | 5.597s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.611s | 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] | 5.506s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 5.584s | passed |
Standard output
1269679 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 1269679 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 1269679 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.9ns 1269694 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1275073 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.39s 1275104 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1275104 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.39ms 1275214 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17177332640703590702.key 1275214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17177332640703590702.key 1275214 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 322ns 1275214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1280576 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.36s 1280607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_17177332640703590702.key 1280607 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1280717 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 1280717 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 1280717 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.7ns 1280717 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1286000 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s 1286016 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1286063 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.14ms 1286172 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_13563015892184566876.key 1286172 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_13563015892184566876.key 1286172 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.6ns 1286172 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1291614 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.43s 1291629 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_13563015892184566876.key 1291629 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1291739 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_11994686858194159975.key 1291739 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_11994686858194159975.key 1291739 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 497.4ns 1291739 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1297212 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.48s 1297243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_11994686858194159975.key 1297243 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1297353 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_3003243523656199859.key 1297353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_3003243523656199859.key 1297353 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.8ns 1297353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1302808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.45s 1302840 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_3003243523656199859.key 1302840 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1302950 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2617547640352421120.key 1302950 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2617547640352421120.key 1302950 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.8ns 1302950 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1308421 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.47s 1308452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_2617547640352421120.key 1308452 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.3ns 1308561 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_2159607180782500506.key 1308561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_2159607180782500506.key 1308561 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.4ns 1308561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1313926 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.36s 1313942 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_2159607180782500506.key 1313958 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1314067 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_823890722616584387.key 1314067 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_823890722616584387.key 1314067 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.9ns 1314067 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1319508 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.44s 1319539 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_823890722616584387.key 1319539 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.1ns 1319651 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_12989219627144279777.key 1319651 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_12989219627144279777.key 1319651 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.5ns 1319651 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1325189 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.54s 1325204 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_12989219627144279777.key 1325220 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.3ns 1325329 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 1325329 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 1325329 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.8ns 1325329 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1330848 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.52s 1330864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1330879 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 1330989 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_9584767711244732283.key 1330989 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_9584767711244732283.key 1330989 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.4ns 1330989 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1336461 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.46s 1336477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_9584767711244732283.key 1336477 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1336586 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_7523284847045131856.key 1336586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_7523284847045131856.key 1336586 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.5ns 1336586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1341934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.35s 1341949 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_7523284847045131856.key 1341949 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1342074 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_6301331911985629943.key 1342074 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_6301331911985629943.key 1342074 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.4ns 1342074 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1347516 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.44s 1347547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_6301331911985629943.key 1347547 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1347656 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12027115849558184172.key 1347656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12027115849558184172.key 1347656 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.1ns 1347656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1353210 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.55s 1353224 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_12027115849558184172.key 1353224 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1353333 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_2646189466270669381.key 1353333 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_2646189466270669381.key 1353333 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.6ns 1353333 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1358821 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.49s 1358852 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_2646189466270669381.key 1358852 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1358962 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_551054101160999518.key 1358962 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_551054101160999518.key 1358962 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.2ns 1358962 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1364402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.45s 1364433 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_551054101160999518.key 1364433 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1364543 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_1982941877027784539.key 1364543 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_1982941877027784539.key 1364543 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 271ns 1364543 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1369968 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.42s 1369985 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_1982941877027784539.key 1369985 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 117ns 1370109 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6480070375322224284.key 1370109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6480070375322224284.key 1370109 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.6ns 1370109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1375535 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.42s 1375566 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_6480070375322224284.key 1375566 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1375675 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4946052994583994969.key 1375675 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4946052994583994969.key 1375675 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.4ns 1375675 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1381164 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.49s 1381195 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_4946052994583994969.key 1381195 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 1381304 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_17178229963440835883.key 1381304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_17178229963440835883.key 1381304 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.8ns 1381304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1386793 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.48s 1386808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_17178229963440835883.key 1386808 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1386918 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_2986015395649074161.key 1386918 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_2986015395649074161.key 1386918 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 376ns 1386918 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1392515 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.59s 1392562 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_2986015395649074161.key 1392562 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ns 1392671 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_5144323872932468909.key 1392671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_5144323872932468909.key 1392671 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.4ns 1392671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1398112 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.43s 1398128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_5144323872932468909.key 1398128 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1398237 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_4650442754105339144.key 1398237 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_4650442754105339144.key 1398237 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.9ns 1398237 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1403693 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.46s 1403709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_4650442754105339144.key 1403725 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1403834 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6962002126973746631.key 1403834 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6962002126973746631.key 1403834 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 557.7ns 1403834 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1409324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.48s 1409339 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_6962002126973746631.key 1409339 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns