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.424s | 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.440s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.486s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.394s | 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.363s | 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.424s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.392s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.472s | 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.409s | 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.393s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.667s | 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.377s | 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.346s | 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.377s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.377s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.425s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.407s | 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.486s | 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.660s | 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.595s | 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.659s | 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.471s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.440s | 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.533s | 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.520s | passed |
Standard output
809459 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 809459 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 809459 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 809459 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 812995 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 813010 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 813010 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.44ms 813120 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_12971606921701393712.key 813120 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_12971606921701393712.key 813120 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.5ns 813120 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 816481 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 816497 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_12971606921701393712.key 816497 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 816606 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 816606 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 816606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.3ns 816606 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 820125 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 820140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 820156 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.27ms 820266 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_9912553319638122580.key 820266 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_9912553319638122580.key 820266 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.2ns 820266 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 823720 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 823752 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_9912553319638122580.key 823752 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.2ns 823861 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_16271346202033837073.key 823861 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_16271346202033837073.key 823861 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.3ns 823861 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 827395 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 827410 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_16271346202033837073.key 827410 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 827520 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12977478891203699298.key 827520 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12977478891203699298.key 827520 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229ns 827520 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 830850 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 830881 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_12977478891203699298.key 830881 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 830991 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_4103245475349687096.key 830991 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_4103245475349687096.key 830991 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.4ns 830991 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 834306 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 834321 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_4103245475349687096.key 834321 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 834431 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15912260911709284933.key 834431 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15912260911709284933.key 834431 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.4ns 834431 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 837839 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 837855 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_15912260911709284933.key 837855 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 837964 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_7390942846095889449.key 837964 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_7390942846095889449.key 837964 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.4ns 837964 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 841343 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 841374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_7390942846095889449.key 841374 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 841484 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_15495238155871761162.key 841484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_15495238155871761162.key 841484 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.5ns 841484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 844783 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 844798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_15495238155871761162.key 844798 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 844908 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 844908 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 844908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.9ns 844908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 848206 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 848222 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 848237 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.18ms 848348 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_18323512827283745579.key 848348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_18323512827283745579.key 848348 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.6ns 848348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 851693 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 851725 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_18323512827283745579.key 851725 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 851834 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_9676851460759775263.key 851834 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_9676851460759775263.key 851834 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 354.7ns 851834 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 855102 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 855117 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_9676851460759775263.key 855117 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 855228 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_6761600315208537147.key 855228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_6761600315208537147.key 855228 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.8ns 855228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 858466 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 858482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_6761600315208537147.key 858482 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 858591 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6257770302210327648.key 858591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6257770302210327648.key 858591 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.9ns 858591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 861890 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 861906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_6257770302210327648.key 861906 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 862015 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4930396232954851700.key 862015 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4930396232954851700.key 862015 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.4ns 862015 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 865283 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 865298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_4930396232954851700.key 865298 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 865408 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2345774016741180482.key 865408 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2345774016741180482.key 865408 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.9ns 865408 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 868755 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 868770 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_2345774016741180482.key 868770 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.5ns 868880 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_10864048980751663191.key 868880 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_10864048980751663191.key 868880 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.3ns 868880 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 872164 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 872180 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_10864048980751663191.key 872180 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 872289 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_10548470260615947717.key 872289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_10548470260615947717.key 872289 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.6ns 872289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 875542 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 875557 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_10548470260615947717.key 875557 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 875682 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14526171833714115188.key 875682 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14526171833714115188.key 875682 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.3ns 875682 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 878934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 878950 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_14526171833714115188.key 878950 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 879059 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11145561778291293624.key 879059 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11145561778291293624.key 879059 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.1ns 879059 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 882279 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 882295 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_11145561778291293624.key 882295 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 882405 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_522600139883236186.key 882405 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_522600139883236186.key 882405 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.9ns 882405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 885657 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 885672 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_522600139883236186.key 885672 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13ns 885782 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_7177889422132855431.key 885782 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_7177889422132855431.key 885782 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233ns 885782 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 889034 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 889050 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_7177889422132855431.key 889050 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 889159 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_17302488701207567340.key 889159 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_17302488701207567340.key 889159 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.8ns 889159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 892443 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 892459 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_17302488701207567340.key 892459 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 892584 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7994244002789502521.key 892584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7994244002789502521.key 892584 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.2ns 892584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 895866 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 895881 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_7994244002789502521.key 895881 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns