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.460s | 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.196s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.338s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.643s | 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.419s | 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.535s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.798s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.528s | 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.728s | 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.576s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.466s | 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.541s | 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.655s | 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.304s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.274s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.270s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.223s | 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.265s | 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.293s | 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.237s | 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.226s | 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.151s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.237s | 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.194s | 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.315s | passed |
Standard output
1241333 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 1241333 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 1241333 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.6ns 1241333 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1246648 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.32s 1246664 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1246679 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.52ms 1246792 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_11745373469056273723.key 1246792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_11745373469056273723.key 1246792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.4ns 1246792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1251931 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.13s 1251947 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_11745373469056273723.key 1251947 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1252058 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 1252058 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 1252058 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.4ns 1252058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1257180 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s 1257211 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1257243 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.44ms 1257352 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3502116127673165369.key 1257352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3502116127673165369.key 1257352 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.4ns 1257352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1262458 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 1262474 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_3502116127673165369.key 1262474 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 1262589 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_1498206805493620564.key 1262589 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_1498206805493620564.key 1262589 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.9ns 1262589 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1267674 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.09s 1267705 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_1498206805493620564.key 1267705 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13ns 1267815 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10230867242382959993.key 1267815 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10230867242382959993.key 1267815 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.9ns 1267815 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1272825 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1272841 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_10230867242382959993.key 1272856 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1272966 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2853784922067276930.key 1272966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2853784922067276930.key 1272966 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.9ns 1272966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1278063 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 1278094 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_2853784922067276930.key 1278094 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70ns 1278203 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6917788761247072130.key 1278203 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6917788761247072130.key 1278203 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.7ns 1278203 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1283272 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.06s 1283287 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_6917788761247072130.key 1283287 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 1283397 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_381522768833171062.key 1283397 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_381522768833171062.key 1283397 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.8ns 1283397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1288584 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s 1288599 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_381522768833171062.key 1288599 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1288712 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_7769135962895242121.key 1288712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_7769135962895242121.key 1288712 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 354.1ns 1288712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1294045 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.33s 1294061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_7769135962895242121.key 1294061 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.2ns 1294173 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 1294173 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 1294173 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.8ns 1294173 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1299238 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.06s 1299254 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1299254 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 1299369 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_9767553701426597339.key 1299369 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_9767553701426597339.key 1299369 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.4ns 1299369 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1304566 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 1304597 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_9767553701426597339.key 1304597 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 1304707 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13529395788477381760.key 1304707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13529395788477381760.key 1304707 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.4ns 1304707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1310224 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.51s 1310240 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_13529395788477381760.key 1310240 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.3ns 1310350 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_8956034375332797328.key 1310350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_8956034375332797328.key 1310350 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.7ns 1310350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1315623 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s 1315655 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_8956034375332797328.key 1315655 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1315769 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15127795869495609594.key 1315769 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15127795869495609594.key 1315769 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.1ns 1315769 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1321177 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.4s 1321193 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_15127795869495609594.key 1321193 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1321304 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_252754860454987056.key 1321304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_252754860454987056.key 1321304 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.76ms 1321304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1326977 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.66s 1326993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_252754860454987056.key 1326993 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 1327103 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_14159248716183988388.key 1327103 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_14159248716183988388.key 1327103 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254ns 1327103 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1332492 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.39s 1332507 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_14159248716183988388.key 1332523 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 1332632 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_8243943347778009625.key 1332632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_8243943347778009625.key 1332632 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.7ns 1332632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1338229 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.59s 1338244 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_8243943347778009625.key 1338244 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.8ns 1338360 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2901086601217839699.key 1338360 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2901086601217839699.key 1338360 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.7ns 1338360 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1343796 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.44s 1343828 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_2901086601217839699.key 1343828 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1343937 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4408616572094922446.key 1343937 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4408616572094922446.key 1343937 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.9ns 1343937 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1349337 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.4s 1349353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_4408616572094922446.key 1349368 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.4ns 1349478 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1401959283293593455.key 1349478 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1401959283293593455.key 1349478 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.9ns 1349478 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1354990 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.52s 1355024 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_1401959283293593455.key 1355024 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.8ns 1355133 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_5318267468786063253.key 1355133 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_5318267468786063253.key 1355133 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.4ns 1355133 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1360296 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s 1360329 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_5318267468786063253.key 1360329 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.7ns 1360437 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_16903846680278885311.key 1360437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_16903846680278885311.key 1360437 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.8ns 1360437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1365583 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.14s 1365598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_16903846680278885311.key 1365598 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ns 1365711 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_15629056365519274553.key 1365711 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_15629056365519274553.key 1365711 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.1ns 1365711 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1370854 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.14s 1370870 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_15629056365519274553.key 1370870 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.5ns 1370982 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_1444882555875862144.key 1370982 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_1444882555875862144.key 1370982 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.7ns 1370982 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1376065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.09s 1376097 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_1444882555875862144.key 1376097 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns