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.392s | 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.456s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.423s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.424s | 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.424s | 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.362s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.440s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.392s | 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.361s | 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.456s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.596s | 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.407s | 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.361s | 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.378s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.362s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.298s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.285s | 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.598s | 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.538s | 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.485s | 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.455s | 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.409s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.424s | 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.424s | 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.394s | passed |
Standard output
809195 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 809195 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 809195 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.2ns 809195 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 812657 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 812672 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 812688 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.07ms 812797 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_852869936716126895.key 812797 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_852869936716126895.key 812797 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.1ns 812797 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 816254 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 816270 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_852869936716126895.key 816286 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 816395 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 816395 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 816395 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.6ns 816395 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 819792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 819808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 819823 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.77ms 819933 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_6392566916762851490.key 819933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_6392566916762851490.key 819933 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.6ns 819933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 823279 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 823310 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_6392566916762851490.key 823310 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 90.9ns 823419 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8948124953387360659.key 823419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8948124953387360659.key 823419 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.2ns 823419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 826749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 826764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_8948124953387360659.key 826764 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 826874 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10844301160980230263.key 826874 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10844301160980230263.key 826874 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.3ns 826874 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 830142 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 830173 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_10844301160980230263.key 830173 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 830283 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_13209475586576407537.key 830283 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_13209475586576407537.key 830283 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.6ns 830283 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 833582 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 833598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_13209475586576407537.key 833598 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 833707 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_17838672155764147121.key 833707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_17838672155764147121.key 833707 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.1ns 833707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 837006 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 837022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_17838672155764147121.key 837022 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 837131 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_2249975835248643540.key 837131 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_2249975835248643540.key 837131 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.2ns 837131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 840400 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 840415 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_2249975835248643540.key 840415 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 840525 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13020374640727819470.key 840525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13020374640727819470.key 840525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.2ns 840525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 843792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 843807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_13020374640727819470.key 843807 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 843917 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 843917 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 843917 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 843917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 847248 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 847263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 847263 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 847373 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_6806239222536745134.key 847373 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_6806239222536745134.key 847373 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.1ns 847373 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 850671 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 850687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_6806239222536745134.key 850687 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 850796 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_6467700842888614451.key 850796 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_6467700842888614451.key 850796 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.9ns 850796 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 854094 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 854110 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_6467700842888614451.key 854110 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 854220 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_4641748271709659792.key 854220 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_4641748271709659792.key 854220 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.6ns 854220 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 857519 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 857535 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_4641748271709659792.key 857535 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 857644 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_10872951852555257429.key 857644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_10872951852555257429.key 857644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251ns 857644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 860881 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 860897 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_10872951852555257429.key 860897 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 861006 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_5157596745503191374.key 861006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_5157596745503191374.key 861006 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.3ns 861006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 864321 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 864338 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_5157596745503191374.key 864338 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 864447 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_12702673120551224816.key 864447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_12702673120551224816.key 864447 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.4ns 864447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 867714 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 867730 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_12702673120551224816.key 867730 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 867839 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15923859920356179676.key 867839 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15923859920356179676.key 867839 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.3ns 867839 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 871075 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 871091 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_15923859920356179676.key 871091 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 871200 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_9439698939217993561.key 871200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_9439698939217993561.key 871200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.7ns 871200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 874484 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 874500 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_9439698939217993561.key 874500 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 874656 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13677052065188842085.key 874656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13677052065188842085.key 874656 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 521.3ns 874656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 877939 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 877954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_13677052065188842085.key 877954 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.5ns 878064 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_13654956714109208941.key 878064 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_13654956714109208941.key 878064 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.8ns 878064 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 881300 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 881316 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_13654956714109208941.key 881316 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 881425 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_1924245116310327938.key 881425 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_1924245116310327938.key 881425 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.4ns 881425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 884678 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 884694 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_1924245116310327938.key 884694 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 884803 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15647351816335168771.key 884803 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15647351816335168771.key 884803 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.3ns 884803 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 888024 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 888040 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_15647351816335168771.key 888040 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 888165 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_7697379423696251873.key 888165 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_7697379423696251873.key 888165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.2ns 888165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 891338 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 891354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_7697379423696251873.key 891354 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51ns 891463 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7859345607971686381.key 891463 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_7859345607971686381.key 891463 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.8ns 891463 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 894623 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 894638 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_7859345607971686381.key 894638 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns