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] | 4.789s | 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] | 4.755s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.695s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.633s | 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] | 4.826s | 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] | 4.766s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.753s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.879s | 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] | 4.915s | 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] | 4.925s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.021s | 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] | 4.942s | 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] | 4.840s | 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.868s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.828s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.868s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.637s | 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] | 4.926s | 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] | 4.910s | 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] | 4.952s | 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] | 4.900s | 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] | 4.796s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.815s | 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] | 4.887s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 4.823s | passed |
Standard output
1085710 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 1085710 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 1085710 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.7ns 1085726 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1090599 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.88s 1090615 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1090630 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 1090740 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_16313102627226299315.key 1090740 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_16313102627226299315.key 1090740 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.7ns 1090740 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1095541 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.79s 1095556 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_16313102627226299315.key 1095556 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 1095668 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 1095668 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 1095668 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.9ns 1095668 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1100422 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.74s 1100437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1100453 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.04ms 1100578 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_4458696393616324194.key 1100578 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_4458696393616324194.key 1100578 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 457.8ns 1100578 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1105402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.82s 1105418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_4458696393616324194.key 1105418 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.3ns 1105531 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_256761031821511983.key 1105531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_256761031821511983.key 1105531 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 946.3ns 1105531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1110304 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.76s 1110319 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_256761031821511983.key 1110319 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ns 1110432 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7025923065944336031.key 1110432 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7025923065944336031.key 1110432 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.2ns 1110432 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1115088 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.66s 1115103 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_7025923065944336031.key 1115120 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.7ns 1115228 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3872975070524883443.key 1115228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3872975070524883443.key 1115228 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.5ns 1115228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1119916 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 1119932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_3872975070524883443.key 1119932 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1120043 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3015432269944505142.key 1120043 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3015432269944505142.key 1120043 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.3ns 1120043 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1124801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.76s 1124817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_3015432269944505142.key 1124817 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1124930 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_4228619126696837990.key 1124930 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_4228619126696837990.key 1124930 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 280ns 1124930 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1129612 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 1129628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_4228619126696837990.key 1129644 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1129753 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_1661039339050204480.key 1129753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_1661039339050204480.key 1129753 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 441.5ns 1129753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1134409 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.65s 1134424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_1661039339050204480.key 1134424 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1134543 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 1134543 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 1134543 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.4ns 1134543 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1139157 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.61s 1139173 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1139189 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 1139298 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_1714667905439686246.key 1139298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_1714667905439686246.key 1139298 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 418.2ns 1139298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1143852 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.56s 1143868 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_1714667905439686246.key 1143884 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1143993 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_10470646531260649385.key 1143993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_10470646531260649385.key 1143993 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.2ns 1143993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1148494 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.5s 1148510 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_10470646531260649385.key 1148510 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 1148626 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11529575371769163857.key 1148626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11529575371769163857.key 1148626 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.1ns 1148626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1153324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.69s 1153340 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_11529575371769163857.key 1153340 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.7ns 1153452 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11279115675416219481.key 1153452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11279115675416219481.key 1153452 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.8ns 1153452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1158093 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.63s 1158109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_11279115675416219481.key 1158109 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1158218 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_17605861605458020397.key 1158218 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_17605861605458020397.key 1158218 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 458.9ns 1158218 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1162831 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.62s 1162862 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_17605861605458020397.key 1162862 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 1162972 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_1045088328327174874.key 1162972 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_1045088328327174874.key 1162972 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.6ns 1162972 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1167711 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.74s 1167742 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_1045088328327174874.key 1167742 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1167851 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_13743802871124045451.key 1167851 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_13743802871124045451.key 1167851 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 282ns 1167851 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1172625 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.78s 1172656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_13743802871124045451.key 1172656 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.8ns 1172766 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_897784792780867433.key 1172766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_897784792780867433.key 1172766 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.5ns 1172766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1177565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.79s 1177580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_897784792780867433.key 1177580 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.4ns 1177691 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11424893933492251154.key 1177691 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11424893933492251154.key 1177691 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 443ns 1177691 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1182493 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.81s 1182524 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_11424893933492251154.key 1182524 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 1182633 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_4110410886703526946.key 1182633 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_4110410886703526946.key 1182633 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.9ns 1182633 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1187349 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.71s 1187366 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_4110410886703526946.key 1187366 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ns 1187473 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_10821600204829816922.key 1187473 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_10821600204829816922.key 1187473 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.7ns 1187473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1192200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.73s 1192231 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_10821600204829816922.key 1192231 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.9ns 1192341 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_352632969577545752.key 1192341 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_352632969577545752.key 1192341 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.7ns 1192341 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1197043 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.7s 1197059 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_352632969577545752.key 1197059 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1197170 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_6312647898593929277.key 1197170 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_6312647898593929277.key 1197170 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.1ns 1197170 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1201897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.73s 1201913 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_6312647898593929277.key 1201913 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1202039 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_15234861742200935732.key 1202039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_15234861742200935732.key 1202039 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.8ns 1202039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1206552 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.5s 1206567 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_15234861742200935732.key 1206567 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns