ProveSMTLemmasTest
|
100%
successful |
Tests
| Test | Method name | Duration | Result |
|---|---|---|---|
| [10] wellFormed.dl, \forall Heap h; \forall Object o; \forall Field f; (wellFormed(h) -> boolean::select(h, (java.lang.Object::select(h, o, f))<<Trigger>>, java.lang.Object::<created>) = TRUE | (java.lang.Object::select(h, o, f)) = null) | testSMTLemmaSoundness(String, String)[10] | 2.769s | 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] | 2.751s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.720s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.751s | 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] | 2.766s | 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] | 2.766s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.798s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.736s | 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] | 2.767s | 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] | 2.751s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.848s | 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] | 2.751s | 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] | 2.737s | 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] | 2.752s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.736s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.753s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.813s | 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] | 2.860s | 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] | 2.845s | 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] | 2.828s | 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] | 2.797s | passed |
| [6] allFields.dl, \forall Object o; \forall Field f; \forall Object o2; ( elementOf(o,f, allFields(o2))<<Trigger>> <-> o = o2 ) | testSMTLemmaSoundness(String, String)[6] | 2.782s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.752s | 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] | 2.752s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 2.735s | passed |
Standard output
643760 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 643760 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 643760 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 643776 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 646496 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 646512 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 646512 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 646621 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10206546876359886764.key 646621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10206546876359886764.key 646621 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227ns 646621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 649326 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 649342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_10206546876359886764.key 649342 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 649468 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 649468 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 649468 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.5ns 649468 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 652157 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 652172 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 652204 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.08ms 652313 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_4858927132613217275.key 652313 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_4858927132613217275.key 652313 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.4ns 652313 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 655017 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 655033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_4858927132613217275.key 655033 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 655142 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_15109024742193223773.key 655142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_15109024742193223773.key 655142 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.7ns 655142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 657815 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 657831 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_15109024742193223773.key 657831 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 657940 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_14068644000011090240.key 657940 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_14068644000011090240.key 657940 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.8ns 657940 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 660597 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 660613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_14068644000011090240.key 660613 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 660722 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_16423237278798155419.key 660722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_16423237278798155419.key 660722 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.9ns 660722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 663349 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 663364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_16423237278798155419.key 663364 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 663474 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_10435008117246082903.key 663474 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_10435008117246082903.key 663474 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.9ns 663474 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 666101 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 666117 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_10435008117246082903.key 666117 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 666226 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_18261708266761704427.key 666226 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_18261708266761704427.key 666226 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.8ns 666226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 668837 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 668853 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_18261708266761704427.key 668853 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 668962 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4084200676426732739.key 668962 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4084200676426732739.key 668962 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.9ns 668962 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 671606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 671621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_4084200676426732739.key 671621 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 671731 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 671731 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 671731 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 298ns 671731 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 674310 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 674357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 674372 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 674482 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_7495398967408611233.key 674482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_7495398967408611233.key 674482 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.4ns 674482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 677078 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 677093 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_7495398967408611233.key 677093 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 677203 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_10839760916655150535.key 677203 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_10839760916655150535.key 677203 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.1ns 677203 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 679829 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 679845 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_10839760916655150535.key 679845 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 679954 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_13148918337082155624.key 679954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_13148918337082155624.key 679954 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.9ns 679954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 682581 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 682596 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_13148918337082155624.key 682612 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 682721 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12772209083953280468.key 682721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12772209083953280468.key 682721 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.6ns 682721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 685363 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 685379 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_12772209083953280468.key 685379 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 685489 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13995959479391503596.key 685489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13995959479391503596.key 685489 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 204ns 685489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 688162 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 688177 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_13995959479391503596.key 688177 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 688287 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_14117727082465501533.key 688287 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_14117727082465501533.key 688287 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.8ns 688287 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 690898 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 690914 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_14117727082465501533.key 690914 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 691023 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_14008489192139468380.key 691023 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_14008489192139468380.key 691023 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 223ns 691023 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 693665 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 693680 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_14008489192139468380.key 693680 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 693790 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15812377182413910440.key 693790 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15812377182413910440.key 693790 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.8ns 693790 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 696417 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 696432 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_15812377182413910440.key 696432 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 696542 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_17083605489904628981.key 696542 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_17083605489904628981.key 696542 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.6ns 696542 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 699153 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 699168 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_17083605489904628981.key 699184 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 699293 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11248211552848790809.key 699293 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11248211552848790809.key 699293 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.9ns 699293 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 701906 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 701921 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_11248211552848790809.key 701921 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 702031 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_16177120714256285384.key 702031 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_16177120714256285384.key 702031 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.3ns 702031 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 704657 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 704673 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_16177120714256285384.key 704673 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 704782 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15899277070769121118.key 704782 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15899277070769121118.key 704782 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.8ns 704782 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 707393 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 707408 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_15899277070769121118.key 707408 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 707518 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_12922007926836188990.key 707518 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_12922007926836188990.key 707518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.8ns 707518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 710146 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 710161 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_12922007926836188990.key 710161 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 710271 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_2845665082305340556.key 710271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_2845665082305340556.key 710271 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.2ns 710271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 712960 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 712975 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_2845665082305340556.key 712975 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns