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.125s | 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.120s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.120s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.141s | 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.077s | 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.131s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.091s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.075s | 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.093s | 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.073s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.360s | 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.135s | 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.154s | 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.147s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.108s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.155s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.149s | 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.211s | 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.156s | 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.174s | 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.161s | 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.127s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.118s | 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.127s | 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.157s | passed |
Standard output
1158978 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 1158978 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 1158978 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 1158994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1164202 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.22s 1164234 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1164234 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms 1164344 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13043561199648921001.key 1164344 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13043561199648921001.key 1164344 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.4ns 1164344 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1169430 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.08s 1169446 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_13043561199648921001.key 1169446 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.4ns 1169555 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 1169555 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 1169555 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.9ns 1169555 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1174567 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 1174583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1174599 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.11ms 1174711 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_16773134237157812888.key 1174711 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_16773134237157812888.key 1174711 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 257ns 1174711 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1179759 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.04s 1179774 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_16773134237157812888.key 1179774 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1179885 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12367899024386105775.key 1179885 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12367899024386105775.key 1179885 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 409.7ns 1179885 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1184919 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 1184934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_12367899024386105775.key 1184934 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1185047 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7209318676122521139.key 1185047 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7209318676122521139.key 1185047 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 402ns 1185047 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1190047 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 1190063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_7209318676122521139.key 1190063 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1190174 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10474883493149194932.key 1190174 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10474883493149194932.key 1190174 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.7ns 1190174 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1195164 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.99s 1195179 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_10474883493149194932.key 1195179 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1195292 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_7916069763208037746.key 1195292 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_7916069763208037746.key 1195292 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.5ns 1195292 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1200289 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 1200304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_7916069763208037746.key 1200304 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1200419 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_12553213988648316064.key 1200419 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_12553213988648316064.key 1200419 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 481ns 1200419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1205436 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s 1205467 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_12553213988648316064.key 1205467 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1205576 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_2802191725578984746.key 1205576 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_2802191725578984746.key 1205576 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.8ns 1205576 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1210576 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.99s 1210592 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_2802191725578984746.key 1210592 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1210703 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 1210703 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 1210703 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.6ns 1210703 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1215682 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1215698 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1215713 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 1215823 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14209867444679905773.key 1215823 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14209867444679905773.key 1215823 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.4ns 1215823 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1220818 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.99s 1220834 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_14209867444679905773.key 1220834 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 1220944 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_3985159285533783970.key 1220944 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_3985159285533783970.key 1220944 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.3ns 1220944 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1225960 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1225975 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_3985159285533783970.key 1225975 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 1226085 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_2130722503497750443.key 1226085 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_2130722503497750443.key 1226085 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.1ns 1226085 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1231035 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s 1231051 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_2130722503497750443.key 1231051 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1231162 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_5956921305859660096.key 1231162 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_5956921305859660096.key 1231162 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 367ns 1231162 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1236153 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.99s 1236185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_5956921305859660096.key 1236185 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1236294 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_12392258547163810275.key 1236294 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_12392258547163810275.key 1236294 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 721ns 1236294 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1241258 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 1241274 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_12392258547163810275.key 1241274 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 1241386 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_5684582382450688154.key 1241386 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_5684582382450688154.key 1241386 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 373ns 1241386 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1246336 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 1246352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_5684582382450688154.key 1246352 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1246462 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_16219400277430890761.key 1246462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_16219400277430890761.key 1246462 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.7ns 1246462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1251430 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 1251445 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_16219400277430890761.key 1251445 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 1251555 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4499418987662334721.key 1251555 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4499418987662334721.key 1251555 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 465.2ns 1251555 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1256489 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s 1256520 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_4499418987662334721.key 1256520 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20ns 1256629 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_1359043209949176910.key 1256629 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_1359043209949176910.key 1256629 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.4ns 1256629 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1261638 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 1261654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_1359043209949176910.key 1261654 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1261764 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11304514078017360202.key 1261764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11304514078017360202.key 1261764 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.2ns 1261764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1266788 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s 1266803 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_11304514078017360202.key 1266803 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 1266918 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_3711786276935501006.key 1266918 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_3711786276935501006.key 1266918 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.2ns 1266918 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1271924 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1271956 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_3711786276935501006.key 1271956 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 1272065 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6262773133017563865.key 1272065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6262773133017563865.key 1272065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.6ns 1272065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1277049 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1277064 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_6262773133017563865.key 1277064 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1277174 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_5590710875580721645.key 1277174 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_5590710875580721645.key 1277174 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.9ns 1277174 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1282202 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 1282218 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_5590710875580721645.key 1282218 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1282331 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12184546181290195861.key 1282331 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12184546181290195861.key 1282331 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.1ns 1282331 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1287351 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s 1287366 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_12184546181290195861.key 1287366 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns