ProveSMTLemmasTest
|
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.328s | 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.330s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.303s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.253s | 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.310s | 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.297s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.299s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.291s | 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.283s | 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.259s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.331s | 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.259s | 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.259s | 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.196s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.299s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.264s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.268s | 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.371s | 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.356s | 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.286s | 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.324s | 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.264s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.273s | 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.251s | 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.278s | passed |
Standard output
978208 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 978208 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 978208 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 978209 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 982413 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.2s 982429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 982435 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.39ms 982539 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_4589628050892590913.key 982540 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_4589628050892590913.key 982540 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.91ns 982541 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 986788 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 986804 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_4589628050892590913.key 986805 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 986909 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 986910 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 986910 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.11ns 986911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 991132 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 991148 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 991160 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.94ms 991266 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_12942815574878561917.key 991266 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_12942815574878561917.key 991266 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.11ns 991267 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 995431 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.16s 995446 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_12942815574878561917.key 995448 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 995552 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_9384686930884905134.key 995552 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_9384686930884905134.key 995552 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.81ns 995553 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 999752 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.2s 999768 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_9384686930884905134.key 999769 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 999876 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_7517274696944439259.key 999876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_7517274696944439259.key 999876 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.71ns 999878 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1004021 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 1004036 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_7517274696944439259.key 1004037 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 1004140 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_9393892252020940713.key 1004141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_9393892252020940713.key 1004141 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 1004141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1008293 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.15s 1008308 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_9393892252020940713.key 1008309 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1008414 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_9221078384629790421.key 1008414 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_9221078384629790421.key 1008414 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 1008415 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1012545 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 1012561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_9221078384629790421.key 1012562 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1012665 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_3314686296706576632.key 1012666 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_3314686296706576632.key 1012666 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.01ns 1012667 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1016824 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.16s 1016839 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_3314686296706576632.key 1016840 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1016943 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_10438053353484802630.key 1016944 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_10438053353484802630.key 1016944 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.11ns 1016945 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1021150 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.2s 1021166 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_10438053353484802630.key 1021167 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1021271 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 1021272 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 1021272 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.21ns 1021273 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1025479 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.21s 1025494 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1025497 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 889.85ns 1025602 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_13997515591377911234.key 1025602 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_13997515591377911234.key 1025602 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 1025603 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1029787 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 1029802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_13997515591377911234.key 1029803 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1029906 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_14414477808989993152.key 1029906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_14414477808989993152.key 1029906 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.21ns 1029907 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1034038 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 1034053 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_14414477808989993152.key 1034055 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1034158 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_17636651603505882461.key 1034158 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_17636651603505882461.key 1034159 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.81ns 1034160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1038348 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s 1038364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_17636651603505882461.key 1038365 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1038468 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_10112322188155333299.key 1038468 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_10112322188155333299.key 1038468 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.01ns 1038470 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1042644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 1042660 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_10112322188155333299.key 1042662 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1042766 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_4698811139280634580.key 1042766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_4698811139280634580.key 1042766 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.91ns 1042768 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1046945 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 1046960 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_4698811139280634580.key 1046962 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1047066 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_18360956004075971345.key 1047066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_18360956004075971345.key 1047066 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 1047067 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1051237 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 1051252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_18360956004075971345.key 1051254 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1051356 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_11164391757713167106.key 1051357 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_11164391757713167106.key 1051357 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.31ns 1051358 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1055520 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.16s 1055535 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_11164391757713167106.key 1055536 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 1055639 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_11152610730105312955.key 1055640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_11152610730105312955.key 1055640 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 1055641 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1059779 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 1059794 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_11152610730105312955.key 1059795 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 1059898 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_3118573708916720445.key 1059898 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_3118573708916720445.key 1059898 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 1059900 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1064036 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 1064052 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_3118573708916720445.key 1064054 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 1064158 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_9648467302773709111.key 1064158 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_9648467302773709111.key 1064158 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.11ns 1064160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1068297 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 1068312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_9648467302773709111.key 1068314 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 1068417 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_5926533530553837550.key 1068418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_5926533530553837550.key 1068418 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.82ns 1068420 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1072493 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.07s 1072508 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_5926533530553837550.key 1072509 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1072612 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_9074704365143732825.key 1072612 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_9074704365143732825.key 1072613 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 1072614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1076792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 1076807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_9074704365143732825.key 1076808 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1076912 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_10605662443329469265.key 1076912 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_10605662443329469265.key 1076912 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.91ns 1076913 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1081056 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 1081071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_10605662443329469265.key 1081072 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1081179 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_4365526886176345046.key 1081179 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_4365526886176345046.key 1081179 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 1081180 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1085327 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.15s 1085342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_4365526886176345046.key 1085343 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns