ProveSMTLemmasTest

all > de.uka.ilkd.key.smt.newsmt2 > ProveSMTLemmasTest
25

tests
0

failures
0

ignored
1m8.01s

duration
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.720s 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.720s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 2.722s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 2.688s 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.705s 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.720s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 2.717s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 2.704s 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.674s 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.720s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 2.697s 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.720s 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.704s 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.721s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 2.689s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 2.719s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 2.704s 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.753s 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.783s 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.768s 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.704s 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.768s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 2.766s 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.736s 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.688s passed

Standard output

642687     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 
642687     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 
642687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
642702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
645284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
645284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.82ms 
645394     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1990205930305235352.key 
645394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1990205930305235352.key 
645394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.6ns 
645394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
648036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_1990205930305235352.key 
648036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 
648145     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 
648145     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 
648145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.5ns 
648145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
650803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
650819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.76ms 
650929     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_10670525520077906487.key 
650929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_10670525520077906487.key 
650929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.5ns 
650929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
653586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_10670525520077906487.key 
653586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
653696     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_18223407531006273337.key 
653696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_18223407531006273337.key 
653696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.1ns 
653696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
656291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_18223407531006273337.key 
656291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
656400     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_17841216610496142189.key 
656400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_17841216610496142189.key 
656400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.4ns 
656400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
659058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_17841216610496142189.key 
659058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
659168     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_5646873562130980625.key 
659168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_5646873562130980625.key 
659168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.4ns 
659168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
661825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_5646873562130980625.key 
661825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
661935     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13112508301766721494.key 
661935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13112508301766721494.key 
661935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.1ns 
661935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
664561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_13112508301766721494.key 
664561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
664671     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_10416924480306105210.key 
664671     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_10416924480306105210.key 
664671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.5ns 
664671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
667250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_10416924480306105210.key 
667250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
667360     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_7620628333629290790.key 
667360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_7620628333629290790.key 
667360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.4ns 
667360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
669970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_7620628333629290790.key 
669970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
670080     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 
670080     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 
670080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.8ns 
670080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
672691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
672691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
672800     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3535231215681392852.key 
672800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3535231215681392852.key 
672800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 806.2ns 
672800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
675414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_3535231215681392852.key 
675414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
675523     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11868619309312467810.key 
675523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11868619309312467810.key 
675523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.5ns 
675523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
678087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
678102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_11868619309312467810.key 
678102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
678212     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_3856900049215140924.key 
678212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_3856900049215140924.key 
678212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223ns 
678212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
680807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_3856900049215140924.key 
680807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
680917     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_224054912150400714.key 
680917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_224054912150400714.key 
680917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.7ns 
680917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
683512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_224054912150400714.key 
683512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
683637     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14159453875826174398.key 
683637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14159453875826174398.key 
683637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.7ns 
683637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
686247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_14159453875826174398.key 
686247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
686357     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_13602621472512243478.key 
686357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_13602621472512243478.key 
686357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.6ns 
686357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
688953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_13602621472512243478.key 
688953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 
689063     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_8520615459181456417.key 
689063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_8520615459181456417.key 
689063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.7ns 
689063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
691611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
691627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_8520615459181456417.key 
691627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 
691736     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_635334118338414821.key 
691736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_635334118338414821.key 
691736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.1ns 
691736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
694331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_635334118338414821.key 
694331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
694456     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_12370867251492708551.key 
694456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_12370867251492708551.key 
694456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.6ns 
694456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
697067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_12370867251492708551.key 
697067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
697177     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_2628055441813353935.key 
697177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_2628055441813353935.key 
697177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.8ns 
697177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
699772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_2628055441813353935.key 
699772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
699881     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_14662069198845558639.key 
699881     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_14662069198845558639.key 
699881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.5ns 
699881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
702477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
702492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_14662069198845558639.key 
702492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
702602     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_389993253606171393.key 
702602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_389993253606171393.key 
702602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.2ns 
702602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
705166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_389993253606171393.key 
705166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
705291     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_4392343740772420695.key 
705291     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_4392343740772420695.key 
705291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.1ns 
705291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
707902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_4392343740772420695.key 
707902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
708011     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3899855740869111533.key 
708011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3899855740869111533.key 
708011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.3ns 
708011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
710592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
710607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_3899855740869111533.key 
710607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns