ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m28.08s

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.527s 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.492s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 3.498s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 3.518s 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.511s 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.434s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 3.499s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 3.534s 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.475s 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.470s 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.581s 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.547s 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.530s 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.476s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 3.515s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 3.538s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 3.470s passed
[2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[2] 3.639s 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.597s 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.571s 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.556s 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.563s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 3.517s 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.514s 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.511s passed

Standard output

805726     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_5033050247978298739.key 
805726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_5033050247978298739.key 
805726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
805727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
809185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
809201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_5033050247978298739.key 
809203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 
809306     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 
809306     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 
809306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
809307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
812813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
812831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
812842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.45ms 
812945     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 
812945     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 
812945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
812946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
816393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
816408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
816434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.71ms 
816542     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_4242223774831356899.key 
816542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_4242223774831356899.key 
816542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
816543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
819991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
820006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_4242223774831356899.key 
820007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
820114     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_2676158461347601682.key 
820115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_2676158461347601682.key 
820115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.3ns 
820117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
823549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
823565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_2676158461347601682.key 
823566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
823669     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_10157753744844898955.key 
823673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_10157753744844898955.key 
823673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
823674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
827113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
827129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_10157753744844898955.key 
827130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ns 
827232     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_18024234004209400833.key 
827233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_18024234004209400833.key 
827233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 636.49ns 
827234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
830631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
830646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_18024234004209400833.key 
830647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
830750     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_7540842136195299839.key 
830750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_7540842136195299839.key 
830750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
830751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
834143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
834159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_7540842136195299839.key 
834160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 
834263     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_16035250443280008624.key 
834263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_16035250443280008624.key 
834263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
834264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
837655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
837670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_16035250443280008624.key 
837672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
837774     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_4668256977735646904.key 
837774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_4668256977735646904.key 
837775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
837775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
841178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
841193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_4668256977735646904.key 
841195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
841301     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 
841301     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 
841301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
841302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
844667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
844682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
844688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
844794     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_15839335311869209477.key 
844794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_15839335311869209477.key 
844794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.4ns 
844795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
848172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
848187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_15839335311869209477.key 
848189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
848291     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_5319481577098616091.key 
848292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_5319481577098616091.key 
848292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
848293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
851684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
851705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_5319481577098616091.key 
851707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
851811     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_1971224122152737092.key 
851811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_1971224122152737092.key 
851811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
851812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
855201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
855216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_1971224122152737092.key 
855217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 
855320     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_1017366605303012236.key 
855320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_1017366605303012236.key 
855320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
855321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
858635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
858651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_1017366605303012236.key 
858652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
858755     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_8038240102431650699.key 
858758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_8038240102431650699.key 
858758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.2ns 
858759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
862134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
862149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_8038240102431650699.key 
862151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
862253     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_4511177291029094945.key 
862254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_4511177291029094945.key 
862254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
862255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
865668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
865683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_4511177291029094945.key 
865685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
865787     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_10744426787602404186.key 
865788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_10744426787602404186.key 
865788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
865789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
869142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
869158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_10744426787602404186.key 
869160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.5ns 
869262     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_11328434939709732786.key 
869263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_11328434939709732786.key 
869263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
869264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
872612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
872628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_11328434939709732786.key 
872630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ns 
872733     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_2037128103474572991.key 
872733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_2037128103474572991.key 
872733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
872735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
876156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
876173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_2037128103474572991.key 
876176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
876279     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_6539091555520012641.key 
876279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_6539091555520012641.key 
876279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
876280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
879688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
879704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_6539091555520012641.key 
879706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
879809     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_7215799070342065666.key 
879809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_7215799070342065666.key 
879809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
879810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
883166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
883181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_7215799070342065666.key 
883182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
883286     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_16573500802267667770.key 
883287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_16573500802267667770.key 
883287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271ns 
883289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
886681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
886697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_16573500802267667770.key 
886699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 
886801     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_9201510928229291566.key 
886802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_9201510928229291566.key 
886802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
886803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
890219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
890235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_9201510928229291566.key 
890237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
890339     INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_1849282339315209878.key 
890339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_1849282339315209878.key 
890340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
890340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
893690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
893705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_1849282339315209878.key 
893706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns