ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m15.03s

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.945s 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.974s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 3.008s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 2.966s 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.980s 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.017s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 3.067s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 2.988s 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.974s 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.000s 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.967s 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.928s 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.935s 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.999s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 3.018s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 3.005s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 3.020s passed
[2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[2] 3.053s 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.032s 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.002s 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.025s 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.049s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 2.989s 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.018s 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.075s passed

Standard output

717477     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_11715267508973253294.key 
717477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_11715267508973253294.key 
717477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 41.1ns 
717478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
720340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_11715267508973253294.key 
720341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
720444     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 
720444     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 
720444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
720445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
723390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
723394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
723496     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 
723497     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 
723497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.7ns 
723498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
726414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
726425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.21ms 
726529     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_4108197968428125784.key 
726530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_4108197968428125784.key 
726530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.3ns 
726531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
729427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_4108197968428125784.key 
729428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
729531     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_764307643590255939.key 
729532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_764307643590255939.key 
729533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.2ns 
729534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
732439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
732453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_764307643590255939.key 
732454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
732557     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_892150541428319229.key 
732557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_892150541428319229.key 
732557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.4ns 
732558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
735501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_892150541428319229.key 
735502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
735605     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_2739533423083089231.key 
735605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_2739533423083089231.key 
735605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
735606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
738490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_2739533423083089231.key 
738491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 
738594     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_16741532712812495968.key 
738594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_16741532712812495968.key 
738595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.3ns 
738596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
741494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
741507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_16741532712812495968.key 
741509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
741612     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_17865869905724849624.key 
741612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_17865869905724849624.key 
741612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
741613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
744583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_17865869905724849624.key 
744584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
744687     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_12911723926122650115.key 
744687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_12911723926122650115.key 
744687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
744691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
747514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
747528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_12911723926122650115.key 
747530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
747632     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 
747632     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 
747632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
747633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
750497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
750501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
750606     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_15608389405940104079.key 
750607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_15608389405940104079.key 
750607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
750608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
753495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
753510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_15608389405940104079.key 
753511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
753614     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_4088655191190522581.key 
753614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_4088655191190522581.key 
753614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
753615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
756477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_4088655191190522581.key 
756478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
756581     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_2939219220174372349.key 
756581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_2939219220174372349.key 
756581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
756582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
759442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
759456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_2939219220174372349.key 
759458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
759561     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_4699557602306819717.key 
759561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_4699557602306819717.key 
759561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
759562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
762461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
762474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_4699557602306819717.key 
762475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 
762579     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_2390938660004363268.key 
762579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_2390938660004363268.key 
762579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
762580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
765541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_2390938660004363268.key 
765543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.6ns 
765645     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_13847496401885021339.key 
765646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_13847496401885021339.key 
765646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
765647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
768517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
768530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_13847496401885021339.key 
768531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
768634     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_17237815116730615421.key 
768634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_17237815116730615421.key 
768634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
768635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
771490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
771503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_17237815116730615421.key 
771504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.6ns 
771607     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_5947324918861593209.key 
771607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_5947324918861593209.key 
771608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
771609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
774486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
774500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_5947324918861593209.key 
774501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 
774608     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_13647533801915908071.key 
774608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_13647533801915908071.key 
774608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
774609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
777415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
777430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_13647533801915908071.key 
777431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
777536     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_7454932675841700599.key 
777536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_7454932675841700599.key 
777536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
777537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
780353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
780367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_7454932675841700599.key 
780368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
780471     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_13154334020427354877.key 
780472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_13154334020427354877.key 
780472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
780473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
783345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
783366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_13154334020427354877.key 
783368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 
783471     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_6732963444675820475.key 
783471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_6732963444675820475.key 
783471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.7ns 
783472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
786369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
786384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_6732963444675820475.key 
786385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.5ns 
786488     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_17791949440120004120.key 
786488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_17791949440120004120.key 
786489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
786489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
789389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_17791949440120004120.key 
789390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
789493     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_7389465976617633464.key 
789494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_7389465976617633464.key 
789494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
789495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
792397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
792409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_7389465976617633464.key 
792410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns