ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m59.69s

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.781s 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.751s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 4.640s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 4.813s 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.742s 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.746s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 4.837s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 4.718s 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.699s 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.864s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 4.921s 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.794s 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.869s 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.972s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 4.779s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 4.690s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 4.740s 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] 4.897s 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] 4.892s 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] 4.752s 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] 4.649s 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.682s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 4.766s 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] 4.820s passed
[9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) testSMTLemmaSoundness(String, String)[9] 4.876s passed

Standard output

1113049    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 
1113049    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 
1113049    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
1113050    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1117844    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.79s 
1117861    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
1117866    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 
1117970    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_1154617635139212237.key 
1117971    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_1154617635139212237.key 
1117971    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157ns 
1117972    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1122746    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.77s 
1122763    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_1154617635139212237.key 
1122764    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 
1122867    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 
1122867    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 
1122867    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
1122869    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1127624    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.75s 
1127640    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
1127654    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.26ms 
1127760    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_15296234677827892917.key 
1127760    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_15296234677827892917.key 
1127760    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
1127761    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1132367    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.61s 
1132407    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_15296234677827892917.key 
1132408    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ns 
1132511    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_10062568905174063678.key 
1132511    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_10062568905174063678.key 
1132511    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
1132512    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1137040    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.53s 
1137056    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_10062568905174063678.key 
1137058    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ns 
1137161    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_2060323309013102548.key 
1137161    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_2060323309013102548.key 
1137161    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
1137163    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1141721    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.56s 
1141737    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_2060323309013102548.key 
1141739    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 
1141842    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_5543787211715676084.key 
1141843    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_5543787211715676084.key 
1141843    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.5ns 
1141844    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1146489    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.64s 
1146505    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_5543787211715676084.key 
1146506    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 
1146609    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_8689721613776728546.key 
1146609    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_8689721613776728546.key 
1146610    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 535.3ns 
1146611    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1151293    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 
1151311    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_8689721613776728546.key 
1151314    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 
1151428    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_8868291498071595772.key 
1151428    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_8868291498071595772.key 
1151428    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns 
1151430    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1156181    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.75s 
1156200    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_8868291498071595772.key 
1156201    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 
1156305    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_13549972040014866679.key 
1156305    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_13549972040014866679.key 
1156305    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
1156307    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1160964    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.66s 
1160980    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_13549972040014866679.key 
1160982    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 
1161085    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 
1161085    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 
1161085    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
1161087    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1165708    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.62s 
1165727    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
1165730    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
1165837    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_11698953517056196758.key 
1165838    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_11698953517056196758.key 
1165838    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.8ns 
1165839    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1170357    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s 
1170372    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_11698953517056196758.key 
1170374    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 
1170477    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_9657386009461270249.key 
1170478    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_9657386009461270249.key 
1170478    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
1170479    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1175168    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.69s 
1175183    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_9657386009461270249.key 
1175186    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ns 
1175290    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_9026025896358600925.key 
1175290    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_9026025896358600925.key 
1175290    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
1175291    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1179912    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.62s 
1179928    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_9026025896358600925.key 
1179930    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 
1180033    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_11079242010058889269.key 
1180034    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_11079242010058889269.key 
1180034    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.8ns 
1180035    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1184658    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.62s 
1184675    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_11079242010058889269.key 
1184676    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 
1184780    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_12345633423297244405.key 
1184780    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_12345633423297244405.key 
1184780    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
1184781    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1189489    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.71s 
1189506    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_12345633423297244405.key 
1189508    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 
1189618    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_16299943596347439235.key 
1189618    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_16299943596347439235.key 
1189618    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
1189619    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1194213    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.59s 
1194228    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_16299943596347439235.key 
1194229    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 
1194335    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_755334563128870019.key 
1194335    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_755334563128870019.key 
1194335    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.9ns 
1194337    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1198913    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.58s 
1198929    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_755334563128870019.key 
1198931    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 
1199036    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_11968559250257379143.key 
1199036    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_11968559250257379143.key 
1199036    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
1199038    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1203775    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.74s 
1203794    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_11968559250257379143.key 
1203795    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 
1203899    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_8452016556523698945.key 
1203899    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_8452016556523698945.key 
1203899    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
1203902    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1208572    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.67s 
1208588    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_8452016556523698945.key 
1208589    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 
1208692    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_14908569002367165494.key 
1208693    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_14908569002367165494.key 
1208693    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.7ns 
1208694    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1213439    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.74s 
1213457    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_14908569002367165494.key 
1213459    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 
1213562    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_10719329334079437863.key 
1213562    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_10719329334079437863.key 
1213562    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
1213563    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1218409    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.85s 
1218427    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_10719329334079437863.key 
1218428    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ns 
1218534    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_11815761252115698793.key 
1218534    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_11815761252115698793.key 
1218534    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.8ns 
1218535    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1223191    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.66s 
1223208    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_11815761252115698793.key 
1223209    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ns 
1223312    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_6599950973447488480.key 
1223313    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_6599950973447488480.key 
1223313    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.5ns 
1223314    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1227883    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.57s 
1227898    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_6599950973447488480.key 
1227900    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 
1228003    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_7769684875267837138.key 
1228003    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_7769684875267837138.key 
1228003    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
1228004    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1232620    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.62s 
1232636    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_7769684875267837138.key 
1232637    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns