ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m17.90s

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] 3.031s 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.145s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 3.167s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 3.023s 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.046s 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.122s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 3.040s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 3.069s 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.106s 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.088s 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] 3.194s 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.183s 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.228s 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.161s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 3.134s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 3.211s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 3.171s passed
[2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[2] 3.195s 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.128s 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.114s 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.072s 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.097s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 3.080s 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.096s 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.001s passed

Standard output

732433     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_15934121649928558582.key 
732433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_15934121649928558582.key 
732434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns 
732435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
735523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_15934121649928558582.key 
735524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ns 
735627     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 
735627     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 
735628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 523.2ns 
735629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
738709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
738716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.85ms 
738821     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 
738822     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 
738822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
738823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
741789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
741803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
741832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.75ms 
741950     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_2147101376589220616.key 
741950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_2147101376589220616.key 
741950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
741951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
744960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_2147101376589220616.key 
744961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 
745064     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_9218405693559022248.key 
745065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_9218405693559022248.key 
745065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
745065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
748033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_9218405693559022248.key 
748034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ns 
748136     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_17719015650075300903.key 
748137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_17719015650075300903.key 
748137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.4ns 
748139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
751117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
751130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_17719015650075300903.key 
751131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 
751234     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_12056278295816290382.key 
751234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_12056278295816290382.key 
751234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.3ns 
751235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
754196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
754209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_12056278295816290382.key 
754210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 
754313     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_1564000738318280047.key 
754314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_1564000738318280047.key 
754314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.6ns 
754315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
757292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
757306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_1564000738318280047.key 
757307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ns 
757410     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_722520035563114512.key 
757410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_722520035563114512.key 
757410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
757411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
760290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
760304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_722520035563114512.key 
760305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 
760410     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_9088934380517746761.key 
760410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_9088934380517746761.key 
760410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
760411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
763325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
763337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_9088934380517746761.key 
763339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ns 
763441     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 
763442     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 
763442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
763443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
766456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
766472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
766480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.35ms 
766586     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_7865405112098760299.key 
766587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_7865405112098760299.key 
766587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.5ns 
766588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
769635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
769648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_7865405112098760299.key 
769650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 
769753     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_127145820096402201.key 
769754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_127145820096402201.key 
769754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.9ns 
769755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
772660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
772673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_127145820096402201.key 
772675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.5ns 
772778     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_10452489730902979308.key 
772778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_10452489730902979308.key 
772778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
772779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
775707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
775720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_10452489730902979308.key 
775721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 
775824     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_4636242666140939696.key 
775824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_4636242666140939696.key 
775824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
775825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
778828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
778841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_4636242666140939696.key 
778842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ns 
778946     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_9163718349885776558.key 
778946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_9163718349885776558.key 
778946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
778949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
781868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
781881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_9163718349885776558.key 
781883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 
781986     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_17041804470160420425.key 
781986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_17041804470160420425.key 
781986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.1ns 
781987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
784938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
784950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_17041804470160420425.key 
784951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 
785056     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_10938306932421691946.key 
785056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_10938306932421691946.key 
785056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
785057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
788040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
788054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_10938306932421691946.key 
788056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 
788160     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_17466157767059037800.key 
788160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_17466157767059037800.key 
788160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
788161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
791131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
791144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_17466157767059037800.key 
791146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 
791249     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_7279437049526949771.key 
791249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_7279437049526949771.key 
791249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
791250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
794315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
794328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_7279437049526949771.key 
794329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 
794432     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_2168910089051796601.key 
794432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_2168910089051796601.key 
794432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
794433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
797542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
797556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_2168910089051796601.key 
797558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 
797660     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_6052543086129643033.key 
797661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_6052543086129643033.key 
797661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.5ns 
797662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
800704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
800717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_6052543086129643033.key 
800718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ns 
800821     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_10647063940578852449.key 
800821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_10647063940578852449.key 
800821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
800822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
803837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
803851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_10647063940578852449.key 
803852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 
803955     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_9875608793009552888.key 
803955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_9875608793009552888.key 
803955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
803956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
807048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
807062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_9875608793009552888.key 
807063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.5ns 
807166     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_17821139059952238259.key 
807166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_17821139059952238259.key 
807167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.7ns 
807167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
810219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
810233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_17821139059952238259.key 
810235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns