ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m58.71s

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.739s 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.689s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 4.751s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 4.711s 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.812s 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.716s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 4.659s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 4.757s 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.689s 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.758s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 4.816s 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.977s 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.778s 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.658s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 4.586s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 4.662s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 4.717s 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.804s 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.802s 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.788s 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.761s 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.739s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 4.797s 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.798s 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.745s passed

Standard output

1045596    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 
1045596    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 
1045597    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.9ns 
1045598    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1050285    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.69s 
1050302    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
1050308    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.35ms 
1050413    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_3411413466573429916.key 
1050414    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_3411413466573429916.key 
1050414    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
1050415    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1055095    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 
1055111    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_3411413466573429916.key 
1055112    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
1055216    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 
1055217    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 
1055217    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
1055218    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1059882    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.66s 
1059898    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
1059914    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.19ms 
1060018    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_6467986305960294236.key 
1060018    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_6467986305960294236.key 
1060018    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
1060019    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1064687    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.67s 
1064702    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_6467986305960294236.key 
1064703    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
1064807    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_6009131638424518561.key 
1064807    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_6009131638424518561.key 
1064807    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.4ns 
1064808    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1069445    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.64s 
1069463    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_6009131638424518561.key 
1069465    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 
1069568    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_13220052058570043510.key 
1069569    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_13220052058570043510.key 
1069569    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
1069571    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1074182    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.61s 
1074203    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_13220052058570043510.key 
1074204    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 
1074307    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_17756362253917729961.key 
1074308    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_17756362253917729961.key 
1074308    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
1074309    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1078984    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 
1078999    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_17756362253917729961.key 
1079001    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 
1079104    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_1467862603169256498.key 
1079105    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_1467862603169256498.key 
1079105    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.7ns 
1079106    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1083782    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 
1083798    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_1467862603169256498.key 
1083799    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
1083902    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_10445298199845449317.key 
1083903    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_10445298199845449317.key 
1083903    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
1083904    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1088527    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.62s 
1088543    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_10445298199845449317.key 
1088545    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 
1088648    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_16427361431075469724.key 
1088648    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_16427361431075469724.key 
1088648    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
1088650    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1093263    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.61s 
1093280    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_16427361431075469724.key 
1093282    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.7ns 
1093386    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 
1093386    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 
1093386    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
1093387    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1097949    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.56s 
1097966    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
1097971    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 
1098075    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_17975181347640718549.key 
1098075    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_17975181347640718549.key 
1098075    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.3ns 
1098076    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1102707    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.63s 
1102722    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_17975181347640718549.key 
1102723    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
1102827    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_8216368146802870290.key 
1102827    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_8216368146802870290.key 
1102827    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
1102828    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1107418    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.59s 
1107433    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_8216368146802870290.key 
1107434    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
1107539    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_16228621481027628292.key 
1107540    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_16228621481027628292.key 
1107540    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
1107541    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1112226    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.69s 
1112244    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_16228621481027628292.key 
1112246    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
1112349    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_15036511743598663122.key 
1112349    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_15036511743598663122.key 
1112350    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
1112351    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1116945    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.59s 
1116961    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_15036511743598663122.key 
1116962    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 
1117066    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_4278336989132067886.key 
1117067    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_4278336989132067886.key 
1117067    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
1117068    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1121602    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.53s 
1121618    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_4278336989132067886.key 
1121622    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 
1121725    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_10948575990618017180.key 
1121725    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_10948575990618017180.key 
1121725    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
1121726    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1126363    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.64s 
1126378    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_10948575990618017180.key 
1126380    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
1126483    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_7497173936431507003.key 
1126483    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_7497173936431507003.key 
1126483    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
1126484    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1131051    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.57s 
1131066    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_7497173936431507003.key 
1131068    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.1ns 
1131171    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_2100062367691573176.key 
1131172    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_2100062367691573176.key 
1131172    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
1131173    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1135810    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.64s 
1135825    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_2100062367691573176.key 
1135826    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
1135930    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_10551460453961030265.key 
1135930    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_10551460453961030265.key 
1135930    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
1135932    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1140782    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.85s 
1140800    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_10551460453961030265.key 
1140803    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 
1140906    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_11267811687745275447.key 
1140907    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_11267811687745275447.key 
1140907    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
1140908    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1145565    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.66s 
1145580    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_11267811687745275447.key 
1145582    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
1145685    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_12625811189633859588.key 
1145685    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_12625811189633859588.key 
1145685    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.5ns 
1145686    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1150223    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.54s 
1150237    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_12625811189633859588.key 
1150239    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 
1150342    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_12884600374950964103.key 
1150342    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_12884600374950964103.key 
1150343    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
1150344    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1154806    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.46s 
1154821    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_12884600374950964103.key 
1154825    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
1154928    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_2246327408074003075.key 
1154928    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_2246327408074003075.key 
1154928    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
1154929    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1159470    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.54s 
1159485    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_2246327408074003075.key 
1159486    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
1159596    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_51496529040879455.key 
1159597    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_51496529040879455.key 
1159597    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.1ns 
1159599    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1164185    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.59s 
1164204    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_51496529040879455.key 
1164205    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns