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.107s | 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.125s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.134s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.153s | 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.117s | 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.163s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.113s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.083s | 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.049s | 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.036s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.186s | 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.099s | 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.084s | 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] | 4.971s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.024s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.053s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.031s | 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.052s | 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.081s | 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.083s | 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.098s | 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.098s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.093s | 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.175s | 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.067s | passed |
Standard output
1145983 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 1145987 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 1145987 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.3ns 1145987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1151015 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 1151030 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1151046 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 1151155 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13679194798124651933.key 1151155 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13679194798124651933.key 1151155 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.7ns 1151155 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1156076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.92s 1156092 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_13679194798124651933.key 1156092 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 1156207 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 1156207 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 1156207 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 489.6ns 1156207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1161132 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.93s 1161147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1161179 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.03ms 1161288 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15955838946151688815.key 1161288 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15955838946151688815.key 1161288 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.7ns 1161288 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1166246 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 1166261 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_15955838946151688815.key 1166261 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1166371 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_13778021230736521780.key 1166371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_13778021230736521780.key 1166371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.7ns 1166371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1171340 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 1171356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_13778021230736521780.key 1171356 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1171469 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_4521583946319024130.key 1171469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_4521583946319024130.key 1171469 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.1ns 1171469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1176426 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 1176442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_4521583946319024130.key 1176442 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 1176568 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_14251919820492733907.key 1176568 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_14251919820492733907.key 1176568 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.1ns 1176568 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1181529 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 1181544 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_14251919820492733907.key 1181544 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.3ns 1181661 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_11861258237236467246.key 1181661 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_11861258237236467246.key 1181661 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.1ns 1181661 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1186695 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 1186711 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_11861258237236467246.key 1186726 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 1186836 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_2598317419464029680.key 1186836 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_2598317419464029680.key 1186836 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.8ns 1186836 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1191778 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s 1191794 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_2598317419464029680.key 1191794 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1191904 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_10381294476400804941.key 1191904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_10381294476400804941.key 1191904 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.3ns 1191904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1196889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1196895 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_10381294476400804941.key 1196895 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 1197011 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 1197011 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 1197011 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.3ns 1197011 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1201995 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1202011 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1202011 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 1202136 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_16268513951318560972.key 1202136 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_16268513951318560972.key 1202136 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.7ns 1202136 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1207131 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 1207163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_16268513951318560972.key 1207163 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 1207272 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_17819881970126854587.key 1207272 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_17819881970126854587.key 1207272 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.6ns 1207272 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1212297 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s 1212313 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_17819881970126854587.key 1212313 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 1212425 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14713768265785584540.key 1212425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14713768265785584540.key 1212425 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.6ns 1212425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1217403 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1217434 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_14713768265785584540.key 1217434 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1217543 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11720248075861985975.key 1217543 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11720248075861985975.key 1217543 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.9ns 1217543 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1222565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s 1222581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_11720248075861985975.key 1222597 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1222706 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_6286927517202725580.key 1222706 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_6286927517202725580.key 1222706 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 619.8ns 1222706 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1227695 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1227711 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_6286927517202725580.key 1227711 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1227820 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15326163616494922402.key 1227820 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15326163616494922402.key 1227820 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.1ns 1227820 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1232775 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 1232791 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_15326163616494922402.key 1232791 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 1232903 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3841276725291188890.key 1232903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3841276725291188890.key 1232903 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.1ns 1232903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1237811 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 1237843 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_3841276725291188890.key 1237843 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1237952 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_11227051009976158735.key 1237952 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_11227051009976158735.key 1237952 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.3ns 1237952 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1242858 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 1242873 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_11227051009976158735.key 1242873 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1242988 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_5957781937493427161.key 1242988 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_5957781937493427161.key 1242988 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.8ns 1242988 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1247956 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 1247972 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_5957781937493427161.key 1247972 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 1248087 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14480174123798821041.key 1248087 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14480174123798821041.key 1248087 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.7ns 1248087 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1253046 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 1253062 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_14480174123798821041.key 1253062 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1253171 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_11305875816757454765.key 1253171 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_11305875816757454765.key 1253171 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.2ns 1253171 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1258002 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.83s 1258017 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_11305875816757454765.key 1258033 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 1258142 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6318231843512494911.key 1258142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6318231843512494911.key 1258142 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.4ns 1258142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1263038 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 1263053 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_6318231843512494911.key 1263053 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1263166 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_9682477768185138390.key 1263166 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_9682477768185138390.key 1263166 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.5ns 1263166 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1268094 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.92s 1268110 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_9682477768185138390.key 1268110 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1268221 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_9540260950464109293.key 1268221 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_9540260950464109293.key 1268221 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 552.3ns 1268221 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1273113 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 1273128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_9540260950464109293.key 1273128 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns