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.549s | 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.518s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.448s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.695s | 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.524s | 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.552s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.463s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.486s | 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.506s | 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.725s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.706s | 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.653s | 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.499s | 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.456s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.454s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.445s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.480s | 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.592s | 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.641s | 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.465s | 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.472s | 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.564s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.673s | 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.456s | 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.541s | passed |
Standard output
825075 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 825075 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 825075 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.4ns 825091 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 828638 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 828654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 828669 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 828779 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1733034480154935127.key 828779 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1733034480154935127.key 828779 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.7ns 828779 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 832230 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 832261 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_1733034480154935127.key 832261 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 832371 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 832371 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 832371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 832371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 835855 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 835871 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 835902 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.73ms 836012 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_13177895338317789654.key 836012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_13177895338317789654.key 836012 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.4ns 836012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 839346 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 839361 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_13177895338317789654.key 839361 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 248.7ns 839477 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_2015707026817040730.key 839477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_2015707026817040730.key 839477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.4ns 839477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 842808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 842823 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_2015707026817040730.key 842823 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 842949 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_5750587067940377660.key 842949 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_5750587067940377660.key 842949 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.8ns 842949 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 846373 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 846388 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_5750587067940377660.key 846388 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 846513 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3938742367693679261.key 846513 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3938742367693679261.key 846513 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 385ns 846513 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 850046 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 850061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_3938742367693679261.key 850077 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 850187 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_18198023141859522554.key 850187 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_18198023141859522554.key 850187 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.8ns 850187 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 853516 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 853531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_18198023141859522554.key 853531 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 853644 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_7870192094647381824.key 853644 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_7870192094647381824.key 853644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.6ns 853644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 857054 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 857069 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_7870192094647381824.key 857069 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 857185 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13395589211691304506.key 857185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13395589211691304506.key 857185 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.6ns 857185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 860606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 860621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_13395589211691304506.key 860621 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 860734 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 860734 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 860734 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.9ns 860734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 864111 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 864128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 864143 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.23ms 864252 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_4520666572150778143.key 864252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_4520666572150778143.key 864252 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.6ns 864252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 867573 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 867588 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_4520666572150778143.key 867588 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.6ns 867701 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11788918343486289762.key 867701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11788918343486289762.key 867701 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.7ns 867701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 871265 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 871281 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_11788918343486289762.key 871281 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 871396 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_15991072056750869712.key 871396 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_15991072056750869712.key 871396 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 400ns 871396 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 874777 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 874792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_15991072056750869712.key 874808 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 874921 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_10972409261648961552.key 874921 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_10972409261648961552.key 874921 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.8ns 874921 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 878345 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 878361 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_10972409261648961552.key 878361 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 878473 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16959352829835658917.key 878473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16959352829835658917.key 878473 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.3ns 878473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 881796 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 881812 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_16959352829835658917.key 881812 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 881937 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_4798659053364216838.key 881937 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_4798659053364216838.key 881937 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.3ns 881937 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 885283 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 885298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_4798659053364216838.key 885298 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 885423 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_13867794408904491041.key 885423 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_13867794408904491041.key 885423 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 681.4ns 885423 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 888788 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 888819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_13867794408904491041.key 888819 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.7ns 888929 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_11252697742122786813.key 888929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_11252697742122786813.key 888929 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.7ns 888929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 892509 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 892541 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_11252697742122786813.key 892541 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 892654 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_2725510162534272723.key 892654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_2725510162534272723.key 892654 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.2ns 892654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 896180 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 896197 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_2725510162534272723.key 896197 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 896308 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7618268271847995346.key 896308 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7618268271847995346.key 896308 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.3ns 896308 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 899678 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 899694 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_7618268271847995346.key 899694 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 899807 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_117462305558114620.key 899807 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_117462305558114620.key 899807 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 429.5ns 899807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 903123 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 903139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_117462305558114620.key 903155 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 903264 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_18241760851334461687.key 903264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_18241760851334461687.key 903264 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.2ns 903264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 906590 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 906605 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_18241760851334461687.key 906605 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 906718 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_13397773362970390916.key 906718 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_13397773362970390916.key 906718 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 217ns 906718 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 910041 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 910057 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_13397773362970390916.key 910057 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 910166 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_441970689605216821.key 910166 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_441970689605216821.key 910166 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.2ns 910166 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 913509 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 913540 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_441970689605216821.key 913540 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns