ProveSMTLemmasTest

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

tests
0

failures
0

ignored
2m17.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.615s 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] 5.559s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 5.423s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 5.520s 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] 5.390s 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] 5.490s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 5.320s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 5.644s 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] 5.424s 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] 5.572s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 5.396s 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] 5.565s 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.717s 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.563s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 5.488s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 5.521s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 5.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] 5.375s 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.520s 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.703s 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.617s 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.454s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 5.425s 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.280s 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.548s passed

Standard output

1289786    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 
1289787    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 
1289787    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
1289788    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1295054    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.27s 
1295072    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
1295079    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 
1295183    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_4153757417287814007.key 
1295184    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_4153757417287814007.key 
1295184    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
1295185    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1300434    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.25s 
1300453    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_4153757417287814007.key 
1300454    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 
1300557    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 
1300557    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 
1300557    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
1300559    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1305928    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.37s 
1305947    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
1305968    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.44ms 
1306077    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_327588950938506685.key 
1306077    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_327588950938506685.key 
1306078    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.2ns 
1306079    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1311655    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.58s 
1311676    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_327588950938506685.key 
1311677    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ns 
1311781    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_6914962529770309830.key 
1311781    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_6914962529770309830.key 
1311781    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
1311782    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1317272    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.49s 
1317292    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_6914962529770309830.key 
1317294    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.6ns 
1317397    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_11907277968190550837.key 
1317397    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_11907277968190550837.key 
1317400    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.94ms 
1317402    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1322727    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.33s 
1322747    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_11907277968190550837.key 
1322749    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ns 
1322852    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_356214927265897198.key 
1322852    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_356214927265897198.key 
1322852    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
1322853    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1328148    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.29s 
1328167    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_356214927265897198.key 
1328169    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ns 
1328276    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_6808631248559738567.key 
1328276    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_6808631248559738567.key 
1328277    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
1328278    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1333430    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.15s 
1333450    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_6808631248559738567.key 
1333452    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ns 
1333556    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_2716731120771605548.key 
1333556    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_2716731120771605548.key 
1333556    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.6ns 
1333558    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1338947    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.39s 
1338990    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_2716731120771605548.key 
1338999    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.3ns 
1339104    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_6558523528633730937.key 
1339105    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_6558523528633730937.key 
1339105    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
1339106    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1344593    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.49s 
1344613    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_6558523528633730937.key 
1344615    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ns 
1344719    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 
1344719    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 
1344719    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
1344721    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1350149    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.43s 
1350170    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
1350174    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
1350280    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_7766247865765782285.key 
1350281    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_7766247865765782285.key 
1350281    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279ns 
1350283    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1355574    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.29s 
1355595    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_7766247865765782285.key 
1355596    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ns 
1355701    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_2271103905621535364.key 
1355701    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_2271103905621535364.key 
1355701    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
1355703    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1361099    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.4s 
1361117    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_2271103905621535364.key 
1361119    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.1ns 
1361222    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_5098303212131012256.key 
1361222    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_5098303212131012256.key 
1361222    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
1361224    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1366486    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.26s 
1366506    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_5098303212131012256.key 
1366508    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.1ns 
1366611    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_6707408313047328374.key 
1366611    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_6707408313047328374.key 
1366611    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
1366614    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1371961    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.35s 
1371997    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_6707408313047328374.key 
1371998    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ns 
1372102    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_17678345008805530404.key 
1372103    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_17678345008805530404.key 
1372103    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
1372104    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1377299    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 
1377318    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_17678345008805530404.key 
1377319    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ns 
1377423    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_7421878569585578836.key 
1377423    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_7421878569585578836.key 
1377423    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
1377424    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1382942    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.52s 
1382960    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_7421878569585578836.key 
1382963    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.4ns 
1383067    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_5505181160175600168.key 
1383067    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_5505181160175600168.key 
1383067    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.5ns 
1383068    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1388368    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.3s 
1388386    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_5505181160175600168.key 
1388388    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 
1388491    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_2557990751947846006.key 
1388491    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_2557990751947846006.key 
1388491    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.6ns 
1388493    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1393932    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.44s 
1393957    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_2557990751947846006.key 
1393959    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 
1394063    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_9415962475564351276.key 
1394063    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_9415962475564351276.key 
1394064    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 651.3ns 
1394066    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1399504    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.44s 
1399523    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_9415962475564351276.key 
1399524    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 
1399627    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_10822609858770369768.key 
1399628    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_10822609858770369768.key 
1399628    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
1399629    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1405220    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.59s 
1405240    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_10822609858770369768.key 
1405242    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 
1405345    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_11491609677394599252.key 
1405346    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_11491609677394599252.key 
1405346    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
1405347    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1410785    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.44s 
1410803    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_11491609677394599252.key 
1410805    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 
1410908    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_7729133771944937513.key 
1410908    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_7729133771944937513.key 
1410908    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
1410910    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1416273    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.36s 
1416291    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_7729133771944937513.key 
1416293    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ns 
1416396    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_18193192438232173838.key 
1416396    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_18193192438232173838.key 
1416396    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
1416397    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1421791    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.39s 
1421812    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_18193192438232173838.key 
1421813    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ns 
1421917    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_2703065687811126112.key 
1421917    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_2703065687811126112.key 
1421917    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
1421918    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1427533    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.61s 
1427552    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_2703065687811126112.key 
1427554    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns