ProveSMTLemmasTest

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

tests
0

failures
0

ignored
2m2.14s

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] 4.965s 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] 4.884s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 4.804s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 4.789s 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] 4.797s 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] 4.859s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 4.607s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 4.607s 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] 4.716s 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] 4.732s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 5.002s 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] 4.726s 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] 4.862s 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] 4.785s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 4.827s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 4.848s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 4.877s passed
[2] seqSub.dl, \forall Seq seq; \forall int from; \forall int to; \forall int idx; any::seqGet(seqSub(seq, from, to)<<Trigger>>, idx) = \if(0 <= idx & idx < (to - from)) \then(any::seqGet(seq, idx + from)) \else(seqGetOutside) testSMTLemmaSoundness(String, String)[2] 5.009s 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] 5.080s 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] 5.083s passed
[5] allFields.dl, \forall Object o; \forall Field f; \forall Object o2; ( elementOf(o,f, allFields(o2))<<Trigger>> <-> o = o2 ) testSMTLemmaSoundness(String, String)[5] 5.010s passed
[6] 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)[6] 5.019s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 5.047s 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] 5.107s passed
[9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) testSMTLemmaSoundness(String, String)[9] 5.096s passed

Standard output

1101970    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 
1101970    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 
1101970    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
1101971    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1106847    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.88s 
1106862    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
1106868    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.33ms 
1106972    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_968825620850801563.key 
1106972    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_968825620850801563.key 
1106972    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
1106973    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1111857    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.88s 
1111876    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_968825620850801563.key 
1111877    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 
1111980    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 
1111980    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 
1111980    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
1111982    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1116921    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s 
1116939    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
1116954    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.87ms 
1117060    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_5415169158068409843.key 
1117060    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_5415169158068409843.key 
1117060    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
1117061    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1122020    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 
1122036    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_5415169158068409843.key 
1122038    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 
1122144    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_7597630024727726438.key 
1122144    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_7597630024727726438.key 
1122144    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
1122145    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1127031    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 
1127048    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_7597630024727726438.key 
1127050    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
1127153    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_14527534667296489224.key 
1127154    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_14527534667296489224.key 
1127154    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
1127155    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1132023    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.87s 
1132067    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_14527534667296489224.key 
1132068    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 
1132172    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_15821701937993502645.key 
1132172    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_15821701937993502645.key 
1132172    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
1132173    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1137098    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.93s 
1137115    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_15821701937993502645.key 
1137116    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 
1137219    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_4924794386366147790.key 
1137220    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_4924794386366147790.key 
1137220    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
1137221    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1142205    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 
1142221    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_4924794386366147790.key 
1142223    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 
1142326    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_6508691708618485311.key 
1142327    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_6508691708618485311.key 
1142327    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
1142328    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1147301    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 
1147317    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_6508691708618485311.key 
1147319    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 
1147423    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_3724987260325106094.key 
1147423    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_3724987260325106094.key 
1147423    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.5ns 
1147424    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1152264    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.84s 
1152283    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_3724987260325106094.key 
1152284    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 
1152389    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 
1152390    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 
1152390    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
1152391    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1157148    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.76s 
1157163    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
1157167    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
1157273    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_10553085748881073291.key 
1157273    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_10553085748881073291.key 
1157273    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
1157274    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1161957    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 
1161973    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_10553085748881073291.key 
1161974    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
1162077    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_2017522695306118536.key 
1162078    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_2017522695306118536.key 
1162078    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
1162079    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1166746    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.67s 
1166762    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_2017522695306118536.key 
1166763    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 
1166866    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_6008580843211178105.key 
1166866    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_6008580843211178105.key 
1166866    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
1166867    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1171543    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 
1171559    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_6008580843211178105.key 
1171560    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
1171663    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_9341648316539370802.key 
1171664    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_9341648316539370802.key 
1171664    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
1171665    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1176400    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.74s 
1176417    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_9341648316539370802.key 
1176419    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 
1176523    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_8395095447899737606.key 
1176523    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_8395095447899737606.key 
1176524    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
1176526    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1181007    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.48s 
1181024    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_8395095447899737606.key 
1181026    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 
1181130    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_18145392355017134983.key 
1181131    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_18145392355017134983.key 
1181131    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.5ns 
1181133    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1185616    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.48s 
1185631    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_18145392355017134983.key 
1185633    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28ns 
1185737    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_8609575799565860539.key 
1185737    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_8609575799565860539.key 
1185737    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
1185739    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1190334    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.59s 
1190349    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_8609575799565860539.key 
1190350    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ns 
1190454    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_3767013759652623389.key 
1190454    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_3767013759652623389.key 
1190454    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
1190455    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1195065    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.61s 
1195081    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_3767013759652623389.key 
1195083    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 
1195186    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_13756280954772282041.key 
1195186    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_13756280954772282041.key 
1195186    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
1195187    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1199783    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.6s 
1199799    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_13756280954772282041.key 
1199801    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 
1199911    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_9935599028577475251.key 
1199911    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_9935599028577475251.key 
1199912    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
1199913    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1204652    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.74s 
1204668    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_9935599028577475251.key 
1204670    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 
1204773    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_15533669154313868378.key 
1204773    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_15533669154313868378.key 
1204773    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
1204774    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1209438    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.66s 
1209454    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_15533669154313868378.key 
1209455    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 
1209558    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_7659546669222962891.key 
1209559    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_7659546669222962891.key 
1209559    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
1209561    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1214262    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.7s 
1214278    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_7659546669222962891.key 
1214281    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 
1214388    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_16951297024281446286.key 
1214389    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_16951297024281446286.key 
1214389    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
1214390    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1219114    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.72s 
1219130    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_16951297024281446286.key 
1219132    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 
1219239    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_18303821610677597064.key 
1219239    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_18303821610677597064.key 
1219245    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 6.07ms 
1219246    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1223993    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.75s 
1224010    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_18303821610677597064.key 
1224011    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns