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.568s | 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.652s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.549s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.534s | 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.573s | 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.485s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.549s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.564s | 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.525s | 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.702s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.699s | 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.582s | 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.521s | 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.493s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.521s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.491s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.457s | 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.620s | 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.754s | 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.670s | 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.537s | 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.532s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.588s | 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.597s | 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.474s | passed |
Standard output
745732 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 745732 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 745732 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.6ns 745740 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 749247 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 749263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 749309 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.9ms 749425 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_9304132262661620158.key 749425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_9304132262661620158.key 749425 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.5ns 749425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 752904 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 752919 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_9304132262661620158.key 752935 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 753060 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 753060 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 753060 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.1ns 753068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 756606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 756622 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 756684 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.43ms 756800 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15597014948066433207.key 756800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15597014948066433207.key 756800 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 347ns 756800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 760333 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 760364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_15597014948066433207.key 760364 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 760473 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_382871418903207699.key 760473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_382871418903207699.key 760473 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.2ns 760473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 763885 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 763901 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_382871418903207699.key 763901 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 764010 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_17953105898492499473.key 764010 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_17953105898492499473.key 764010 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 131ns 764010 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 767402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 767418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_17953105898492499473.key 767434 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.6ns 767543 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_18052779940141334521.key 767543 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_18052779940141334521.key 767543 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 237ns 767543 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 771004 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 771020 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_18052779940141334521.key 771020 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.2ns 771132 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13541464333503127297.key 771132 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13541464333503127297.key 771132 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.5ns 771132 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 774603 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 774619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_13541464333503127297.key 774619 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.4ns 774729 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_11205911571848817587.key 774729 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_11205911571848817587.key 774729 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.6ns 774729 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 778075 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 778090 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_11205911571848817587.key 778090 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 277ns 778204 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_11364714242949327615.key 778204 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_11364714242949327615.key 778204 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 276ns 778204 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 781647 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 781663 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_11364714242949327615.key 781663 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 781772 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 781772 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 781772 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.7ns 781772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 785294 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 785310 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 785310 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.64ms 785424 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_17253792714432698933.key 785424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_17253792714432698933.key 785424 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.9ns 785424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 788832 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 788848 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_17253792714432698933.key 788863 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 788973 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13485973512980095370.key 788973 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13485973512980095370.key 788973 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.5ns 788973 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 792382 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 792397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_13485973512980095370.key 792397 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 792507 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17737473336128692652.key 792507 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17737473336128692652.key 792507 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.4ns 792507 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 795951 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 795967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_17737473336128692652.key 795967 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 796081 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_16683881836350361498.key 796081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_16683881836350361498.key 796081 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.4ns 796081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 799435 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 799450 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_16683881836350361498.key 799450 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 799566 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_859787839620063423.key 799566 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_859787839620063423.key 799566 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 431.6ns 799566 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 802975 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 802995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_859787839620063423.key 802995 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 803257 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_8241588602174688274.key 803257 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_8241588602174688274.key 803257 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.6ns 803257 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 806666 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 806682 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_8241588602174688274.key 806682 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 806794 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_16702092287278488278.key 806794 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_16702092287278488278.key 806794 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.1ns 806794 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 810195 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 810211 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_16702092287278488278.key 810211 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 810320 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_14331388307272009854.key 810320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_14331388307272009854.key 810320 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 308ns 810320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 813882 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 813897 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_14331388307272009854.key 813913 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 814022 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_1092672274279680321.key 814022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_1092672274279680321.key 814022 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 467.1ns 814022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 817464 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 817480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_1092672274279680321.key 817480 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 817605 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_18382942603269873626.key 817605 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_18382942603269873626.key 817605 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.4ns 817605 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 820997 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 821013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_18382942603269873626.key 821013 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 821126 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_3463501577965378874.key 821126 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_3463501577965378874.key 821126 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.7ns 821126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 824494 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 824510 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_3463501577965378874.key 824510 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 824619 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_460225441390208321.key 824619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_460225441390208321.key 824619 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 481ns 824619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 828001 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 828016 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_460225441390208321.key 828032 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 828141 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_15089004865728249530.key 828141 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_15089004865728249530.key 828141 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 291ns 828141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 831507 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 831507 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_15089004865728249530.key 831523 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 831632 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12283818944808198220.key 831632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12283818944808198220.key 831632 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.5ns 831632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 834965 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 834981 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_12283818944808198220.key 834981 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns