ProveSMTLemmasTest

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

tests
0

failures
0

ignored
2m2.37s

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.886s 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.872s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 4.838s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 5.031s 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.895s 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.835s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 4.922s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 4.856s 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.855s 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.885s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 4.853s 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.890s 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.810s 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.875s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 4.885s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 4.790s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 4.902s 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.928s 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.979s 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.045s 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.015s 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.913s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 4.891s 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.831s 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.890s passed

Standard output

1130399    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 
1130399    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 
1130400    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.2ns 
1130401    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1135126    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.73s 
1135141    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
1135146    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
1135250    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_11361194415095184035.key 
1135251    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_11361194415095184035.key 
1135251    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
1135252    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1140057    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.81s 
1140074    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_11361194415095184035.key 
1140075    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.7ns 
1140178    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 
1140178    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 
1140178    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.9ns 
1140179    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1145022    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.84s 
1145037    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
1145051    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ms 
1145157    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_7502861271632958154.key 
1145158    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_7502861271632958154.key 
1145158    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106ns 
1145159    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1150080    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.92s 
1150095    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_7502861271632958154.key 
1150099    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.5ns 
1150203    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_9971651804562747865.key 
1150203    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_9971651804562747865.key 
1150203    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
1150204    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1155099    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s 
1155114    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_9971651804562747865.key 
1155115    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
1155218    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_15000532450909425491.key 
1155218    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_15000532450909425491.key 
1155218    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.2ns 
1155220    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1160011    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.79s 
1160027    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_15000532450909425491.key 
1160028    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
1160131    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_16849612042479334661.key 
1160131    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_16849612042479334661.key 
1160131    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
1160132    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1164880    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.75s 
1164918    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_16849612042479334661.key 
1164919    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
1165023    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_7373336893829388876.key 
1165023    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_7373336893829388876.key 
1165023    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
1165024    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1169733    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.71s 
1169749    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_7373336893829388876.key 
1169750    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
1169854    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_17412071987811007498.key 
1169854    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_17412071987811007498.key 
1169854    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
1169855    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1174623    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.77s 
1174639    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_17412071987811007498.key 
1174640    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
1174743    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_9512882300935584879.key 
1174744    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_9512882300935584879.key 
1174744    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
1174745    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1179509    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.76s 
1179525    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_9512882300935584879.key 
1179526    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
1179628    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 
1179629    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 
1179629    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
1179630    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1184380    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.75s 
1184395    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
1184398    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
1184501    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_1407810828102000791.key 
1184502    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_1407810828102000791.key 
1184502    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
1184503    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1189219    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.72s 
1189235    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_1407810828102000791.key 
1189237    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
1189340    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_7002109243433542307.key 
1189340    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_7002109243433542307.key 
1189340    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
1189341    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1194250    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 
1194267    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_7002109243433542307.key 
1194268    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
1194371    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_11709875604560747100.key 
1194371    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_11709875604560747100.key 
1194372    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
1194373    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1199144    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.77s 
1199161    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_11709875604560747100.key 
1199162    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
1199265    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_9021160097769641185.key 
1199266    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_9021160097769641185.key 
1199266    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
1199267    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1203980    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.71s 
1203996    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_9021160097769641185.key 
1203997    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
1204101    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_7660160981894263747.key 
1204101    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_7660160981894263747.key 
1204102    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 746.39ns 
1204103    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1208902    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.8s 
1208918    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_7660160981894263747.key 
1208920    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
1209023    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_15117343552640483987.key 
1209023    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_15117343552640483987.key 
1209024    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.3ns 
1209024    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1213760    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.74s 
1213775    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_15117343552640483987.key 
1213776    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 
1213879    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_3894501402137653120.key 
1213880    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_3894501402137653120.key 
1213881    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.2ns 
1213882    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1218615    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.73s 
1218630    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_3894501402137653120.key 
1218632    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 
1218734    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_15935923749892144852.key 
1218735    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_15935923749892144852.key 
1218735    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
1218736    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1223495    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.76s 
1223511    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_15935923749892144852.key 
1223512    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
1223620    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_17447090791554069229.key 
1223620    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_17447090791554069229.key 
1223620    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
1223621    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1228386    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.76s 
1228401    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_17447090791554069229.key 
1228403    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
1228509    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_7233975205309903333.key 
1228510    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_7233975205309903333.key 
1228510    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
1228512    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1233196    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 
1233213    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_7233975205309903333.key 
1233214    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
1233320    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_14308527630872958438.key 
1233320    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_14308527630872958438.key 
1233320    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.8ns 
1233321    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1238072    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.75s 
1238087    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_14308527630872958438.key 
1238089    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
1238195    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_1166217232026935958.key 
1238195    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_1166217232026935958.key 
1238195    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
1238196    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1242957    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.76s 
1242973    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_1166217232026935958.key 
1242976    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 
1243080    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_14438428240756384390.key 
1243081    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_14438428240756384390.key 
1243081    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
1243082    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1247751    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.67s 
1247766    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_14438428240756384390.key 
1247768    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 
1247871    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_945995706175415461.key 
1247871    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_945995706175415461.key 
1247871    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
1247872    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1252653    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.78s 
1252668    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_945995706175415461.key 
1252670    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.6ns