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.191s | 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] | 3.267s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.268s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.190s | 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.252s | 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.268s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.233s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.252s | 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.269s | 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.283s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.401s | 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.252s | 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.234s | 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.316s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.267s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.266s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.268s | 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.362s | 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.268s | 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.337s | 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.345s | 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.237s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.284s | 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.267s | 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.254s | passed |
Standard output
762528 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 762528 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 762528 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.8ns 762528 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 765780 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 765795 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 765811 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ms 765920 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_12817138438473231074.key 765920 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_12817138438473231074.key 765920 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.3ns 765920 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 769157 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 769172 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_12817138438473231074.key 769172 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 769282 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 769282 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 769282 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.6ns 769282 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 772394 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 772425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 772441 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.41ms 772550 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_4101746369839505675.key 772550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_4101746369839505675.key 772550 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.8ns 772550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 775771 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 775787 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_4101746369839505675.key 775787 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 775887 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12573921081153566260.key 775887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12573921081153566260.key 775887 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.2ns 775887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 779092 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 779123 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_12573921081153566260.key 779123 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 779232 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_518601965663149995.key 779232 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_518601965663149995.key 779232 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.9ns 779232 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 782344 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 782359 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_518601965663149995.key 782359 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 782469 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2127141571302651601.key 782469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2127141571302651601.key 782469 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.3ns 782469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 785628 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 785644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_2127141571302651601.key 785644 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 785753 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15901739262472338517.key 785753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15901739262472338517.key 785753 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.7ns 785753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 788895 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 788911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_15901739262472338517.key 788911 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 789020 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_13815601820418505859.key 789020 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_13815601820418505859.key 789020 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.4ns 789020 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 792149 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 792165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_13815601820418505859.key 792165 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 792274 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_2004234706648441439.key 792274 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_2004234706648441439.key 792274 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.5ns 792274 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 795339 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 795355 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_2004234706648441439.key 795355 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 795465 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 795465 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 795465 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.7ns 795465 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 798591 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 798607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 798622 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 798732 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_1687246065213966096.key 798732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_1687246065213966096.key 798732 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.1ns 798732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 801875 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 801891 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_1687246065213966096.key 801891 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 802000 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_454206130547126897.key 802000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_454206130547126897.key 802000 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 416.9ns 802000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 805065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 805080 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_454206130547126897.key 805080 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 805190 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10269504458745045408.key 805190 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10269504458745045408.key 805190 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 288ns 805190 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 808316 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 808332 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_10269504458745045408.key 808332 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 808442 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_1073902262837240780.key 808442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_1073902262837240780.key 808442 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.8ns 808442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 811585 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 811600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_1073902262837240780.key 811600 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 811710 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4402712926327735813.key 811710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4402712926327735813.key 811710 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.1ns 811710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 814821 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 814837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_4402712926327735813.key 814837 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 814946 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9996740133779997661.key 814946 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9996740133779997661.key 814946 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267ns 814946 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 818073 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 818088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_9996740133779997661.key 818088 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 818198 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_5157662850600904619.key 818198 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_5157662850600904619.key 818198 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 434.7ns 818198 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 821326 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 821341 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_5157662850600904619.key 821341 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.6ns 821467 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_1822306900830647058.key 821467 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_1822306900830647058.key 821467 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 477.9ns 821467 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 824610 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 824641 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_1822306900830647058.key 824641 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 824750 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_9903866475832659953.key 824750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_9903866475832659953.key 824750 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.7ns 824750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 827877 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 827892 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_9903866475832659953.key 827892 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 828002 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9983678296796089362.key 828002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9983678296796089362.key 828002 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 410ns 828002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 831112 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 831128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_9983678296796089362.key 831128 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 831237 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_4172894057534066183.key 831237 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_4172894057534066183.key 831237 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.6ns 831237 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 834412 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 834427 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_4172894057534066183.key 834427 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 834553 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_11161595123403679491.key 834553 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_11161595123403679491.key 834553 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 430.6ns 834553 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 837695 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 837710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_11161595123403679491.key 837710 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 837820 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_624533416882421981.key 837820 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_624533416882421981.key 837820 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 447.4ns 837820 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 840961 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 840977 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_624533416882421981.key 840977 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 841086 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_13870459285675973912.key 841086 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_13870459285675973912.key 841086 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.3ns 841086 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 844229 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 844245 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_13870459285675973912.key 844245 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns