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] | 3.767s | 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.033s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.766s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.816s | 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] | 3.784s | 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] | 3.722s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.718s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.816s | 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] | 3.830s | 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] | 3.768s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.943s | 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] | 3.814s | 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] | 3.862s | 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] | 3.891s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.783s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.878s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.879s | 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] | 3.737s | 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] | 3.955s | 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] | 3.799s | 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] | 3.955s | 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] | 3.798s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.020s | 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] | 3.987s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 3.863s | passed |
Standard output
900065 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 900065 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 900065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.5ns 900065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 903865 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 903881 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 903896 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.79ms 904006 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1093677760131473984.key 904006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1093677760131473984.key 904006 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.56ms 904006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 907618 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 907633 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_1093677760131473984.key 907633 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 907743 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 907743 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 907743 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.8ns 907743 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 911526 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 911542 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 911589 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.13ms 911698 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_11036088619963878936.key 911698 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_11036088619963878936.key 911698 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.8ns 911698 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 915372 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.67s 915387 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_11036088619963878936.key 915387 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.3ns 915497 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_6114492741038950917.key 915497 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_6114492741038950917.key 915497 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.1ns 915497 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 919311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.82s 919342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_6114492741038950917.key 919342 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 919452 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_11558986225478663740.key 919452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_11558986225478663740.key 919452 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.1ns 919452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 923110 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 923142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_11558986225478663740.key 923142 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 923251 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_11656105157363122721.key 923251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_11656105157363122721.key 923251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244ns 923251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 927130 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 927162 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_11656105157363122721.key 927162 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 927271 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_694931189975223398.key 927271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_694931189975223398.key 927271 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 516.3ns 927271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 931133 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.85s 931149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_694931189975223398.key 931149 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 931259 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_1884122232952361770.key 931259 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_1884122232952361770.key 931259 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.4ns 931259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 934997 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 935013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_1884122232952361770.key 935013 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 935122 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4727614042498350852.key 935122 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4727614042498350852.key 935122 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.2ns 935122 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 938749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s 938764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_4727614042498350852.key 938780 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 938889 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 938889 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 938889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.2ns 938889 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 942766 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 942782 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 942813 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.68ms 942923 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_17506545985302453945.key 942923 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_17506545985302453945.key 942923 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 661.8ns 942923 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 946550 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s 946565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_17506545985302453945.key 946581 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 946690 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_2345617186583928828.key 946690 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_2345617186583928828.key 946690 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.4ns 946690 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 950365 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.68s 950381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_2345617186583928828.key 950396 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 950506 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_2426790514720721474.key 950506 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_2426790514720721474.key 950506 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.2ns 950506 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 954165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 954181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_2426790514720721474.key 954181 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 954290 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_14865220278614159207.key 954290 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_14865220278614159207.key 954290 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.6ns 954290 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 957870 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 957902 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_14865220278614159207.key 957902 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 958012 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_755913339186540350.key 958012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_755913339186540350.key 958012 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.1ns 958012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 961606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 961623 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_755913339186540350.key 961623 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.8ns 961731 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_17778935755455968910.key 961731 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_17778935755455968910.key 961731 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.4ns 961731 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 965422 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 965437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_17778935755455968910.key 965437 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 965547 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_10610079382858034225.key 965547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_10610079382858034225.key 965547 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.3ns 965547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 969252 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s 969268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_10610079382858034225.key 969268 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 969377 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8005850851596665306.key 969377 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8005850851596665306.key 969377 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.3ns 969377 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 973004 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s 973020 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_8005850851596665306.key 973020 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 973145 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4065230026620875864.key 973145 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4065230026620875864.key 973145 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.1ns 973145 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 976834 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.68s 976850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_4065230026620875864.key 976850 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 976959 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1661994092090287618.key 976959 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1661994092090287618.key 976959 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.6ns 976959 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 980696 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 980712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_1661994092090287618.key 980712 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 980821 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_12030461573102559368.key 980821 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_12030461573102559368.key 980821 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 430.4ns 980821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 984573 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s 984604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_12030461573102559368.key 984604 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 984713 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_10916497883001835850.key 984713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_10916497883001835850.key 984713 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.9ns 984713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 988371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 988387 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_10916497883001835850.key 988387 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 988496 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_10173622777915767312.key 988496 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_10173622777915767312.key 988496 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.3ns 988496 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 992234 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.74s 992265 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_10173622777915767312.key 992265 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 992374 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7834639473069078353.key 992374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7834639473069078353.key 992374 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.2ns 992374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 996127 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s 996143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_7834639473069078353.key 996143 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.3ns