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] | 2.924s | 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.492s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.109s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.187s | 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.325s | 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.013s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.868s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.302s | 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.362s | 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.086s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.080s | 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.117s | 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.339s | 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.203s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.080s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.364s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.937s | 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.207s | 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.270s | 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.129s | 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.365s | 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] | 2.894s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.089s | 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.421s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 2.960s | passed |
Standard output
758325 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 758325 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 758325 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 117ns 758325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 761266 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 761281 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 761281 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.39ms 761395 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_16886613616766993356.key 761395 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_16886613616766993356.key 761395 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.8ns 761395 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 764477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 764492 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_16886613616766993356.key 764492 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 764602 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 764602 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 764602 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 764602 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 767684 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 767716 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 767762 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.13ms 767872 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_9122402398795701507.key 767872 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_9122402398795701507.key 767872 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.6ns 767872 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 770858 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 770889 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_9122402398795701507.key 770889 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 771001 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8347897321565873972.key 771001 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8347897321565873972.key 771001 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.1ns 771017 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 774235 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 774250 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_8347897321565873972.key 774250 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 774366 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_3830739700245189801.key 774366 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_3830739700245189801.key 774366 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 125ns 774366 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 777133 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 777149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_3830739700245189801.key 777149 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.4ns 777263 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_15768053712549358291.key 777263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_15768053712549358291.key 777263 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.5ns 777263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 780226 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 780241 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_15768053712549358291.key 780241 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 780354 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4396649720849868972.key 780354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4396649720849868972.key 780354 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.5ns 780354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 783647 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 783663 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_4396649720849868972.key 783663 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 783772 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_1335831535848445623.key 783772 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_1335831535848445623.key 783772 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 148ns 783772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 786607 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 786623 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_1335831535848445623.key 786623 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 786733 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5347056923971500723.key 786733 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5347056923971500723.key 786733 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.9ns 786733 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 789491 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 789538 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5347056923971500723.key 789538 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 789657 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 789657 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 789657 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 789657 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 792903 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 792918 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 793046 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 125.85ms 793149 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_13352737519122736742.key 793149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_13352737519122736742.key 793149 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.1ns 793149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 796134 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 796149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_13352737519122736742.key 796149 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 796259 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13812570804074564649.key 796259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13812570804074564649.key 796259 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 206ns 796259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 799320 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 799336 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_13812570804074564649.key 799336 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 799446 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14947945598717035015.key 799446 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14947945598717035015.key 799446 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.9ns 799446 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 802630 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 802646 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_14947945598717035015.key 802662 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 802771 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_17358639196557729132.key 802771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_17358639196557729132.key 802771 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 168ns 802771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 805659 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 805674 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_17358639196557729132.key 805674 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 805784 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_6941644516088282648.key 805784 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_6941644516088282648.key 805784 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.3ns 805784 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 808512 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 808527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_6941644516088282648.key 808527 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 808654 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_13767963330129907036.key 808654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_13767963330129907036.key 808654 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.3ns 808654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 811821 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 811837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_13767963330129907036.key 811837 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 811956 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_6182796629605672330.key 811956 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_6182796629605672330.key 811971 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 23.87ms 811987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 815191 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 815207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_6182796629605672330.key 815207 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 815318 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_7843198927325973796.key 815318 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_7843198927325973796.key 815318 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.4ns 815318 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 818279 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 818294 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_7843198927325973796.key 818294 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 818404 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4757314266947450938.key 818404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4757314266947450938.key 818404 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.3ns 818404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 821380 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 821411 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_4757314266947450938.key 821411 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 821521 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11704223418290741193.key 821521 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11704223418290741193.key 821521 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.2ns 821521 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 824735 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 824750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_11704223418290741193.key 824750 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 824860 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_11783959267696205439.key 824860 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_11783959267696205439.key 824860 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 493.4ns 824860 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 827938 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 827954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_11783959267696205439.key 827954 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 828063 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15602997123161005126.key 828063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15602997123161005126.key 828063 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.5ns 828063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 831003 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 831018 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_15602997123161005126.key 831034 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 831143 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_3551942284079129108.key 831143 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_3551942284079129108.key 831143 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.4ns 831159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 834372 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 834387 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_3551942284079129108.key 834403 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 834512 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_4332176806122018218.key 834512 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_4332176806122018218.key 834512 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.2ns 834512 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 837313 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 837328 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_4332176806122018218.key 837328 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns