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.362s | 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.350s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.310s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.451s | 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.447s | 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.383s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.373s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.416s | 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.418s | 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.418s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.484s | 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.402s | 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.364s | 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.383s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.396s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.371s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.426s | 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.444s | 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.502s | 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.409s | 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.334s | 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.382s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.350s | 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.351s | 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.330s | passed |
Standard output
1228852 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 1228852 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 1228852 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.8ns 1228867 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1234199 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.33s 1234215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1234231 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.72ms 1234340 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8033380214635947143.key 1234340 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8033380214635947143.key 1234340 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.5ns 1234340 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1239660 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.31s 1239675 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_8033380214635947143.key 1239675 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1239785 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 1239785 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 1239785 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 841.3ns 1239785 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1245145 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.35s 1245160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1245176 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.41ms 1245288 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3612917949299438727.key 1245288 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3612917949299438727.key 1245288 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.2ns 1245288 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1250556 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.27s 1250587 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_3612917949299438727.key 1250587 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1250697 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_18180411206382143697.key 1250697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_18180411206382143697.key 1250697 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.9ns 1250697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1255903 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 1255918 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_18180411206382143697.key 1255918 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 1256031 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_13240444292278185963.key 1256031 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_13240444292278185963.key 1256031 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.2ns 1256031 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1261283 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.25s 1261299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_13240444292278185963.key 1261299 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1261413 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6035130659680440493.key 1261413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6035130659680440493.key 1261413 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.5ns 1261413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1266622 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.22s 1266654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_6035130659680440493.key 1266654 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1266763 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13371731433658391726.key 1266763 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13371731433658391726.key 1266763 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 425.1ns 1266763 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1271973 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.21s 1271989 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_13371731433658391726.key 1272004 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1272114 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_1620471844411117445.key 1272114 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_1620471844411117445.key 1272114 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.2ns 1272114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1277303 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.19s 1277319 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_1620471844411117445.key 1277334 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1277444 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13629597886235904498.key 1277444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13629597886235904498.key 1277444 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.4ns 1277444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1282678 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.23s 1282693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_13629597886235904498.key 1282693 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1282806 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 1282806 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 1282806 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.2ns 1282806 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1288016 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.21s 1288031 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1288047 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 1288156 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_1395860074065489711.key 1288156 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_1395860074065489711.key 1288156 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.4ns 1288156 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1293338 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s 1293354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_1395860074065489711.key 1293354 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1293466 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_486450327429793789.key 1293466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_486450327429793789.key 1293466 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.7ns 1293466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1298786 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.32s 1298801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_486450327429793789.key 1298801 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1298917 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_3968243069117758580.key 1298917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_3968243069117758580.key 1298917 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.6ns 1298917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1304237 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.31s 1304253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_3968243069117758580.key 1304253 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15ns 1304364 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9001801414435780863.key 1304364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9001801414435780863.key 1304364 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.3ns 1304364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1309617 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.24s 1309638 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_9001801414435780863.key 1309638 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.7ns 1309747 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9346373663563628696.key 1309747 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9346373663563628696.key 1309747 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.2ns 1309747 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1314981 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.23s 1314997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_9346373663563628696.key 1315012 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 1315122 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_3272136876969227964.key 1315122 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_3272136876969227964.key 1315122 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.7ns 1315122 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1320413 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s 1320429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_3272136876969227964.key 1320429 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 1320538 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_17626598015024863668.key 1320538 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_17626598015024863668.key 1320538 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 310ns 1320538 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1325831 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.29s 1325847 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_17626598015024863668.key 1325847 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.8ns 1325956 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_5829820388669723435.key 1325956 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_5829820388669723435.key 1325956 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.6ns 1325956 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1331234 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s 1331265 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_5829820388669723435.key 1331265 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1331374 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_18317095050951870001.key 1331374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_18317095050951870001.key 1331374 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.2ns 1331374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1336644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.27s 1336661 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_18317095050951870001.key 1336661 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1336777 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5649027834100320515.key 1336777 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5649027834100320515.key 1336777 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.7ns 1336777 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1342014 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.23s 1342029 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_5649027834100320515.key 1342029 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 1342141 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_11365645153931693708.key 1342141 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_11365645153931693708.key 1342141 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 245ns 1342141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1347395 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.25s 1347411 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_11365645153931693708.key 1347411 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1347524 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_16052348979626634859.key 1347524 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_16052348979626634859.key 1347524 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.4ns 1347524 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1352780 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.26s 1352796 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_16052348979626634859.key 1352796 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 1352921 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_3948911375863724783.key 1352921 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_3948911375863724783.key 1352921 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.1ns 1352921 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1358164 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.24s 1358179 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_3948911375863724783.key 1358179 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.2ns 1358292 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_4811574858833104761.key 1358292 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_4811574858833104761.key 1358292 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 497.9ns 1358292 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1363590 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.29s 1363606 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_4811574858833104761.key 1363606 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns