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.134s | 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.147s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.139s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.070s | 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.083s | 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.197s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.137s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.114s | 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.123s | 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.166s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.246s | 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.294s | 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.066s | 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.145s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.156s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.239s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.188s | 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.181s | 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.150s | 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.190s | 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.191s | 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.101s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.119s | 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.088s | 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.086s | passed |
Standard output
1186222 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 1186222 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 1186222 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.5ns 1186235 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1191328 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 1191344 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1191360 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.33ms 1191469 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8048302781457320166.key 1191469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8048302781457320166.key 1191469 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.4ns 1191469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1196505 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.04s 1196520 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_8048302781457320166.key 1196536 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 1196650 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 1196650 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 1196650 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.8ns 1196650 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1201642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.99s 1201658 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1201690 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.92ms 1201800 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_11661744185676599639.key 1201800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_11661744185676599639.key 1201800 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.4ns 1201800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1206860 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.06s 1206876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_11661744185676599639.key 1206876 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1206990 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_1550549679658127165.key 1206990 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_1550549679658127165.key 1206990 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.2ns 1206990 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1212055 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.06s 1212071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_1550549679658127165.key 1212071 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1212181 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7056078303517890449.key 1212181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7056078303517890449.key 1212181 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.7ns 1212181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1217152 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 1217168 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_7056078303517890449.key 1217168 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1217282 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_403709532257346154.key 1217282 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_403709532257346154.key 1217282 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 246ns 1217282 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1222270 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.99s 1222286 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_403709532257346154.key 1222286 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1222401 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_11750230195081510594.key 1222401 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_11750230195081510594.key 1222401 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.5ns 1222401 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1227361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 1227376 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_11750230195081510594.key 1227376 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1227489 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_10446731347729373346.key 1227489 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_10446731347729373346.key 1227489 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.4ns 1227489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1232450 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 1232465 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_10446731347729373346.key 1232465 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1232575 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_12473654418411270650.key 1232575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_12473654418411270650.key 1232575 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.2ns 1232575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1237569 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 1237601 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_12473654418411270650.key 1237601 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1237710 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 1237710 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 1237710 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.1ns 1237710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1242717 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1242732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1242748 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 1242857 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_1181012286531173650.key 1242857 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_1181012286531173650.key 1242857 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.9ns 1242857 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1247867 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1247882 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_1181012286531173650.key 1247882 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1247996 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13246641403441522367.key 1247996 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13246641403441522367.key 1247996 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.1ns 1247996 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1252938 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s 1252956 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_13246641403441522367.key 1252956 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1253066 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_15635276975819871803.key 1253066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_15635276975819871803.key 1253066 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.4ns 1253066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1258019 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 1258035 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_15635276975819871803.key 1258035 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1258149 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_1547505844859947488.key 1258149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_1547505844859947488.key 1258149 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 250ns 1258149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1263221 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.07s 1263237 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_1547505844859947488.key 1263237 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 1263346 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_8193503441000211086.key 1263346 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_8193503441000211086.key 1263346 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 464.2ns 1263346 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1268359 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1268375 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_8193503441000211086.key 1268375 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 1268484 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_7013829226967741518.key 1268484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_7013829226967741518.key 1268484 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.2ns 1268484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1273467 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.99s 1273483 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_7013829226967741518.key 1273483 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1273598 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_1041792796010729499.key 1273598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_1041792796010729499.key 1273598 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 292ns 1273598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1278565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 1278580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_1041792796010729499.key 1278580 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 1278737 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_11494622492533706835.key 1278737 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_11494622492533706835.key 1278737 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 449.2ns 1278737 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1283748 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1283779 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_11494622492533706835.key 1283779 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1283888 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_6649186965438626104.key 1283888 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_6649186965438626104.key 1283888 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 499.7ns 1283888 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1289058 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s 1289074 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_6649186965438626104.key 1289074 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1289183 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_706005560443385415.key 1289183 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_706005560443385415.key 1289183 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.3ns 1289183 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1294118 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s 1294134 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_706005560443385415.key 1294134 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1294249 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_6676279259197172579.key 1294249 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_6676279259197172579.key 1294249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.4ns 1294249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1299253 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1299269 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_6676279259197172579.key 1299269 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1299394 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12171478074209891363.key 1299394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12171478074209891363.key 1299394 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 384ns 1299394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1304425 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 1304441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_12171478074209891363.key 1304441 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1304550 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_14594912057949028645.key 1304550 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_14594912057949028645.key 1304550 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.8ns 1304550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1309665 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.11s 1309680 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_14594912057949028645.key 1309680 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1309790 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_105768846854489621.key 1309790 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_105768846854489621.key 1309790 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.7ns 1309790 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1314853 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.06s 1314869 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_105768846854489621.key 1314869 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns