ProveSMTLemmasTest

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

tests
0

failures
0

ignored
2m5.87s

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] 5.036s 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.935s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 5.068s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 4.962s 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.815s 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.855s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 4.845s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 4.797s 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.637s 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.840s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 5.255s 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.927s 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] 5.016s 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] 5.084s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 5.324s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 5.195s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 5.085s 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.289s 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.419s 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.127s 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.092s 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] 4.982s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 5.130s 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.105s 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.047s passed

Standard output

1155062    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 
1155063    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 
1155064    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.5ns 
1155065    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1160190    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.13s 
1160207    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
1160212    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
1160316    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_9560405791181992362.key 
1160317    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_9560405791181992362.key 
1160317    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
1160318    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1165481    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s 
1165500    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_9560405791181992362.key 
1165502    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 
1165605    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 
1165605    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 
1165606    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.7ns 
1165607    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1170885    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s 
1170901    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
1170917    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.73ms 
1171024    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_5536721834411381612.key 
1171025    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_5536721834411381612.key 
1171025    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
1171026    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1176024    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 
1176046    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_5536721834411381612.key 
1176048    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ns 
1176152    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_1249272875251852090.key 
1176152    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_1249272875251852090.key 
1176152    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
1176153    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1181119    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 
1181138    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_1249272875251852090.key 
1181140    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 
1181243    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_3296642268640643451.key 
1181243    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_3296642268640643451.key 
1181244    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
1181245    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1186100    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.85s 
1186120    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_3296642268640643451.key 
1186122    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.9ns 
1186225    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_1561134690396792959.key 
1186226    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_1561134690396792959.key 
1186226    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
1186227    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1191232    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 
1191251    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_1561134690396792959.key 
1191253    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 
1191356    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_3398370450264342851.key 
1191356    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_3398370450264342851.key 
1191356    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.9ns 
1191358    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1196339    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 
1196356    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_3398370450264342851.key 
1196357    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 
1196461    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_13085338955963684240.key 
1196461    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_13085338955963684240.key 
1196461    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.6ns 
1196462    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1201387    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.92s 
1201403    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_13085338955963684240.key 
1201405    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
1201507    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_5430140680587562436.key 
1201508    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_5430140680587562436.key 
1201508    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
1201512    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1206422    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 
1206438    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5430140680587562436.key 
1206440    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 
1206544    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 
1206545    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 
1206545    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.7ns 
1206546    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1211351    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.81s 
1211370    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
1211374    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
1211478    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_12306096874826454143.key 
1211480    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_12306096874826454143.key 
1211480    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.2ns 
1211481    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1216427    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 
1216443    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_12306096874826454143.key 
1216444    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 
1216548    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_6665607011130893953.key 
1216549    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_6665607011130893953.key 
1216549    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
1216550    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1221386    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.84s 
1221404    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_6665607011130893953.key 
1221405    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 
1221509    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_9894988018792862404.key 
1221509    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_9894988018792862404.key 
1221510    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
1221511    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1226199    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.69s 
1226218    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_9894988018792862404.key 
1226219    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 
1226324    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_7913560846695815303.key 
1226325    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_7913560846695815303.key 
1226325    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
1226326    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1231058    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.73s 
1231075    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_7913560846695815303.key 
1231076    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 
1231180    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_8774663032969485802.key 
1231180    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_8774663032969485802.key 
1231180    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
1231181    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1235902    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.72s 
1235918    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_8774663032969485802.key 
1235921    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 
1236025    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_7559737451316018220.key 
1236026    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_7559737451316018220.key 
1236026    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
1236027    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1240701    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.67s 
1240717    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_7559737451316018220.key 
1240719    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 
1240822    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_6568011625464447571.key 
1240822    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_6568011625464447571.key 
1240822    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
1240823    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1245339    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s 
1245354    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_6568011625464447571.key 
1245355    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 
1245458    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_15752984739174995518.key 
1245458    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_15752984739174995518.key 
1245458    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
1245460    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1250177    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.72s 
1250193    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_15752984739174995518.key 
1250195    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 
1250299    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_15395487375494865079.key 
1250299    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_15395487375494865079.key 
1250299    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
1250300    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1255098    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.8s 
1255117    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_15395487375494865079.key 
1255119    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 
1255227    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_6786888691857389881.key 
1255227    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_6786888691857389881.key 
1255227    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
1255229    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1260119    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 
1260138    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_6786888691857389881.key 
1260139    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 
1260243    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_6243013725726947926.key 
1260243    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_6243013725726947926.key 
1260243    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
1260244    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1265201    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 
1265217    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_6243013725726947926.key 
1265218    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 
1265326    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_6915130931076585055.key 
1265326    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_6915130931076585055.key 
1265326    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
1265328    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1270524    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 
1270541    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_6915130931076585055.key 
1270548    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 
1270651    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_7978097648238493369.key 
1270651    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_7978097648238493369.key 
1270652    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.1ns 
1270652    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1275724    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.07s 
1275739    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_7978097648238493369.key 
1275740    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 
1275852    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_12051753211083022940.key 
1275853    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_12051753211083022940.key 
1275857    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.49ms 
1275858    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1280818    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 
1280834    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_12051753211083022940.key 
1280835    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns