ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m3.54s

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.535s 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.521s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 2.535s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 2.510s 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.534s 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.524s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 2.540s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 2.536s 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.518s 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.532s passed
[1] 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)[1] 2.683s 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.517s 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.529s 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.541s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 2.513s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 2.529s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 2.535s passed
[2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[2] 2.569s 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.611s 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.581s 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.531s 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.549s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 2.515s 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.535s 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.514s passed

Standard output

589434     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_18121630480149276233.key 
589434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_18121630480149276233.key 
589434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 39ns 
589435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
592014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_18121630480149276233.key 
592015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ns 
592117     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jmod.dl.proof 
592117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jmod.dl.proof 
592117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
592118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
594578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
594581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
594686     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_seqGetOutside.dl.proof 
594686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_seqGetOutside.dl.proof 
594686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
594687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
597181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
597191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.15ms 
597297     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_17346529048356539070.key 
597298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_17346529048356539070.key 
597298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 35.1ns 
597298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
599774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_17346529048356539070.key 
599775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ns 
599878     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_1420487131452828078.key 
599878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_1420487131452828078.key 
599878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 40.6ns 
599879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
602306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_1420487131452828078.key 
602307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ns 
602409     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_16614223797491611052.key 
602409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_16614223797491611052.key 
602409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 37.4ns 
602410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
604854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_16614223797491611052.key 
604855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ns 
604957     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_2780597855890045839.key 
604958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_2780597855890045839.key 
604958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 31.7ns 
604959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
607367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_2780597855890045839.key 
607368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ns 
607473     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_11205238570706270136.key 
607473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_11205238570706270136.key 
607473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 35.2ns 
607474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
609905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_11205238570706270136.key 
609906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ns 
610008     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_11742574943910046624.key 
610008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_11742574943910046624.key 
610008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 39.6ns 
610009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
612419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_11742574943910046624.key 
612420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ns 
612522     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_4185297176538180312.key 
612523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_4185297176538180312.key 
612523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.6ns 
612525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
614954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_4185297176538180312.key 
614955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ns 
615061     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jdiv.dl.proof 
615061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/smt/newsmt2/SMT_lemma_jdiv.dl.proof 
615061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.2ns 
615062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
617477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
617479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 877.5ns 
617581     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_13855046937471811485.key 
617581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_13855046937471811485.key 
617581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 33ns 
617582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
620013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_13855046937471811485.key 
620014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.1ns 
620116     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_7936599681411765526.key 
620116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_7936599681411765526.key 
620116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
620117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
622524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_7936599681411765526.key 
622525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ns 
622627     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_5453824510884374930.key 
622627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_5453824510884374930.key 
622627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
622628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
625057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_5453824510884374930.key 
625058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ns 
625160     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_3651306361601355869.key 
625160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_3651306361601355869.key 
625160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 34ns 
625161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
627581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_3651306361601355869.key 
627582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ns 
627684     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_3323383109679436169.key 
627685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_3323383109679436169.key 
627685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.4ns 
627685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
630115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_3323383109679436169.key 
630122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ns 
630224     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_4059084884013561317.key 
630224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_4059084884013561317.key 
630224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45ns 
630225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
632657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_4059084884013561317.key 
632658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ns 
632760     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_5027380452624592164.key 
632760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_5027380452624592164.key 
632760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.7ns 
632761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
635175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_5027380452624592164.key 
635176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 
635277     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_17277045684415456848.key 
635278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_17277045684415456848.key 
635278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 41ns 
635278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
637707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_17277045684415456848.key 
637708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.4ns 
637810     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_8053965000106843699.key 
637810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_8053965000106843699.key 
637810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 33.4ns 
637811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
640224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_8053965000106843699.key 
640225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ns 
640327     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_620373960639947474.key 
640327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_620373960639947474.key 
640327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 41.5ns 
640328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
642754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_620373960639947474.key 
642755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ns 
642857     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_10054713413119378605.key 
642857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_10054713413119378605.key 
642857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 35.8ns 
642858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
645291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_10054713413119378605.key 
645292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ns 
645396     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_12258161755123568541.key 
645396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_12258161755123568541.key 
645397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 40.8ns 
645397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
647807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_12258161755123568541.key 
647808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ns 
647910     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_7378661461580894159.key 
647910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_7378661461580894159.key 
647910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 33ns 
647911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
650338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_7378661461580894159.key 
650339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ns 
650440     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_8114639438623101931.key 
650441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_8114639438623101931.key 
650441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 37.4ns 
650441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
652873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_8114639438623101931.key 
652874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.7ns