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.124s | 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.162s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.168s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.103s | 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.130s | 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.038s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.102s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.106s | 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.092s | 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.132s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.218s | 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.107s | 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.182s | 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.084s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.138s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.149s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.229s | 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.198s | 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.228s | 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.111s | 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.137s | 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.165s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.207s | 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.143s | 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.107s | passed |
Standard output
1169469 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 1169469 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 1169469 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.3ns 1169469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1174535 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.07s 1174551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1174567 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.31ms 1174676 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_16501745173625775203.key 1174676 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_16501745173625775203.key 1174676 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.9ns 1174676 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1179742 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.07s 1179758 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_16501745173625775203.key 1179758 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.7ns 1179874 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 1179874 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 1179874 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.3ns 1179874 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1184941 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.07s 1184957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1184988 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.01ms 1185102 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_12416601851291109536.key 1185102 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_12416601851291109536.key 1185102 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.3ns 1185102 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1190073 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1190088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_12416601851291109536.key 1190104 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1190213 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8046112369158903783.key 1190213 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8046112369158903783.key 1190213 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 429.1ns 1190213 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1195206 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 1195237 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_8046112369158903783.key 1195237 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 180.9ns 1195350 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_16830940493517486079.key 1195350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_16830940493517486079.key 1195350 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.8ns 1195350 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1200375 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 1200390 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_16830940493517486079.key 1200406 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1200515 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_14895465649874069290.key 1200515 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_14895465649874069290.key 1200515 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 303ns 1200515 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1205597 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.08s 1205613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_14895465649874069290.key 1205613 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1205722 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_16873212746062689421.key 1205722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_16873212746062689421.key 1205722 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.8ns 1205722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1210738 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1210754 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_16873212746062689421.key 1210754 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1210865 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_9365812659634766137.key 1210865 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_9365812659634766137.key 1210865 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.5ns 1210865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1215846 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1215861 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_9365812659634766137.key 1215861 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1215972 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_16282887954509765357.key 1215972 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_16282887954509765357.key 1215972 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.1ns 1215972 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1220965 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.99s 1220981 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_16282887954509765357.key 1220981 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 1221096 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 1221096 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 1221096 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258ns 1221096 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1226129 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 1226145 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1226145 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 1226258 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_9522835345421663503.key 1226258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_9522835345421663503.key 1226258 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.6ns 1226258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1231299 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 1231317 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_9522835345421663503.key 1231317 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1231426 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5683024976293121821.key 1231426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5683024976293121821.key 1231426 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.6ns 1231426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1236404 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 1236420 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_5683024976293121821.key 1236420 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1236529 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9886914187978295347.key 1236529 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9886914187978295347.key 1236529 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.6ns 1236529 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1241536 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 1241551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_9886914187978295347.key 1241551 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 1241659 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9146817194107739414.key 1241659 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9146817194107739414.key 1241659 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230ns 1241659 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1246569 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s 1246584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_9146817194107739414.key 1246584 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1246697 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9881960336929720652.key 1246697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9881960336929720652.key 1246697 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.9ns 1246697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1251669 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 1251685 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_9881960336929720652.key 1251685 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1251800 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6336820675838034339.key 1251800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6336820675838034339.key 1251800 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 573.5ns 1251800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1256765 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 1256781 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_6336820675838034339.key 1256781 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1256906 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18410100908504687806.key 1256906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18410100908504687806.key 1256906 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 389.6ns 1256906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1261859 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 1261874 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_18410100908504687806.key 1261874 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1261999 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_658800226806564206.key 1261999 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_658800226806564206.key 1261999 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.7ns 1261999 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1267002 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 1267017 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_658800226806564206.key 1267017 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1267132 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_1884628808942634361.key 1267132 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_1884628808942634361.key 1267132 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.4ns 1267132 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1272098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 1272114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_1884628808942634361.key 1272114 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1272239 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5441579192795446031.key 1272239 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5441579192795446031.key 1272239 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.2ns 1272239 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1277281 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.04s 1277296 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_5441579192795446031.key 1277296 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1277421 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_10231792154391311821.key 1277421 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_10231792154391311821.key 1277421 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.1ns 1277421 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1282364 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s 1282380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_10231792154391311821.key 1282395 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1282505 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_8626910915848971640.key 1282505 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_8626910915848971640.key 1282505 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 402.6ns 1282505 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1287492 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1287533 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_8626910915848971640.key 1287533 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1287643 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_4812248998836532287.key 1287643 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_4812248998836532287.key 1287643 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 384ns 1287643 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1292651 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1292667 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_4812248998836532287.key 1292682 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ns 1292792 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12794030252837121685.key 1292792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12794030252837121685.key 1292792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 556ns 1292792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1297896 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 1297912 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_12794030252837121685.key 1297912 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns