ProveSMTLemmasTest

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

tests
0

failures
0

ignored
1m50.99s

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.362s 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.376s passed
[12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) testSMTLemmaSoundness(String, String)[12] 4.367s passed
[13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) testSMTLemmaSoundness(String, String)[13] 4.355s 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.342s 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.345s passed
[16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 testSMTLemmaSoundness(String, String)[16] 4.347s passed
[17] length.dl, \forall Object o; length(o) >= 0 testSMTLemmaSoundness(String, String)[17] 4.377s 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.354s 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.348s passed
[1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom testSMTLemmaSoundness(String, String)[1] 4.584s 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.356s 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.359s 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.353s passed
[23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x testSMTLemmaSoundness(String, String)[23] 4.367s passed
[24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 testSMTLemmaSoundness(String, String)[24] 4.345s passed
[25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) testSMTLemmaSoundness(String, String)[25] 4.336s 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.562s 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.666s 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.645s 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.838s 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.635s passed
[7] seqEmpty.dl, seqLen(seqEmpty) = 0 testSMTLemmaSoundness(String, String)[7] 4.620s 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.399s 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.350s passed

Standard output

1009324    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 
1009324    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 
1009324    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
1009325    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1013783    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.46s 
1013800    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 
1013805    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
1013910    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_13886097546605857956.key 
1013910    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_13886097546605857956.key 
1013910    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.3ns 
1013912    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1018346    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.43s 
1018366    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_13886097546605857956.key 
1018367    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
1018470    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 
1018470    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 
1018471    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.4ns 
1018474    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1022992    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s 
1023010    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 
1023029    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.02ms 
1023137    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_3647719566154083720.key 
1023137    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_3647719566154083720.key 
1023137    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.7ns 
1023138    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1027658    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s 
1027677    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_3647719566154083720.key 
1027678    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 
1027781    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_14555397964517562573.key 
1027782    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_14555397964517562573.key 
1027782    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
1027784    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1032498    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.71s 
1032516    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_14555397964517562573.key 
1032517    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
1032619    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_8860567714287400934.key 
1032620    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_8860567714287400934.key 
1032620    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
1032621    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1037126    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.5s 
1037145    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_8860567714287400934.key 
1037151    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
1037255    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_79665313366530772.key 
1037259    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_79665313366530772.key 
1037260    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.2ns 
1037261    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1041754    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.49s 
1041771    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_79665313366530772.key 
1041772    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
1041875    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_12276502997297068651.key 
1041875    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_12276502997297068651.key 
1041875    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
1041876    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1046152    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 
1046169    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_12276502997297068651.key 
1046171    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
1046274    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_3857531932795453082.key 
1046274    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_3857531932795453082.key 
1046274    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.1ns 
1046276    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1050502    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 
1050519    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_3857531932795453082.key 
1050520    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 
1050623    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_5678707257057054954.key 
1050624    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_5678707257057054954.key 
1050624    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
1050625    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1054863    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 
1054881    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5678707257057054954.key 
1054882    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
1054985    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 
1054985    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 
1054985    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
1054988    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1059236    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 
1059254    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 
1059257    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
1059362    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_14470139811813554075.key 
1059362    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_14470139811813554075.key 
1059362    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.5ns 
1059364    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1063608    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 
1063624    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_14470139811813554075.key 
1063626    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 
1063729    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_15566243678390588132.key 
1063729    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_15566243678390588132.key 
1063729    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.7ns 
1063730    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1067962    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 
1067979    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_15566243678390588132.key 
1067980    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
1068083    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_187896442977659325.key 
1068083    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_187896442977659325.key 
1068083    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.5ns 
1068084    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1072304    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 
1072321    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_187896442977659325.key 
1072322    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
1072425    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_14422567247911278301.key 
1072426    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_14422567247911278301.key 
1072426    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns 
1072428    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1076649    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 
1076666    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_14422567247911278301.key 
1076667    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
1076771    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_6638397039236609394.key 
1076772    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_6638397039236609394.key 
1076772    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
1076773    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1080993    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 
1081010    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_6638397039236609394.key 
1081012    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
1081118    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_6382107349633796067.key 
1081119    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_6382107349633796067.key 
1081119    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
1081121    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1085373    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 
1085390    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_6382107349633796067.key 
1085391    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
1085496    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_860105857170236609.key 
1085496    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_860105857170236609.key 
1085497    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
1085498    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1089725    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 
1089742    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_860105857170236609.key 
1089743    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 
1089849    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_13261439393946879560.key 
1089849    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_13261439393946879560.key 
1089849    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
1089856    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1094075    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 
1094093    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_13261439393946879560.key 
1094094    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
1094197    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_4162982132513569331.key 
1094198    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_4162982132513569331.key 
1094199    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.13ms 
1094201    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1098432    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 
1098449    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_4162982132513569331.key 
1098450    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
1098554    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_9437433300487828694.key 
1098554    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_9437433300487828694.key 
1098554    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.1ns 
1098556    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1102791    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 
1102808    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_9437433300487828694.key 
1102809    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
1102912    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_14571182668944723376.key 
1102913    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_14571182668944723376.key 
1102913    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
1102914    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1107145    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 
1107162    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_14571182668944723376.key 
1107163    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
1107267    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_7652161299138884300.key 
1107267    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_7652161299138884300.key 
1107267    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
1107269    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1111512    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 
1111529    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_7652161299138884300.key 
1111530    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
1111633    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_14881599043334754563.key 
1111634    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_14881599043334754563.key 
1111634    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
1111635    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1115858    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 
1115875    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_14881599043334754563.key 
1115876    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
1115979    INFO  Test worker     d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_4926966694802413271.key 
1115980    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_4926966694802413271.key 
1115980    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
1115981    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1120194    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.21s 
1120211    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_4926966694802413271.key 
1120212    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns