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.514s | 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.495s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.374s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.372s | 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.420s | 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.357s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.408s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.451s | 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.434s | 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.389s | passed |
| [1] 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)[1] | 4.307s | 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.317s | 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.370s | 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.566s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.344s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.388s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.406s | passed |
| [2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[2] | 4.367s | 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.417s | 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.312s | 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.283s | 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.456s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.297s | 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.436s | 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.317s | passed |
Standard output
976565 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_9354579765910624776.key 976565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_9354579765910624776.key 976566 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.12ns 976567 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 980749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 980767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_9354579765910624776.key 980768 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 980871 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 980872 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 980872 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.51ns 980873 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 985110 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 985130 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 985135 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 985238 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 985238 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 985239 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 985240 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 989516 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 989534 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 989552 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.4ms 989655 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_7924268814553105728.key 989656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_7924268814553105728.key 989656 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 989658 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 993846 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s 993863 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_7924268814553105728.key 993864 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 993968 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_17224590561354567207.key 993968 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_17224590561354567207.key 993969 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.61ns 993970 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 998129 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.16s 998146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_17224590561354567207.key 998147 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 998252 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_6547125543630426310.key 998253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_6547125543630426310.key 998253 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.92ns 998259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1002583 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.32s 1002601 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_6547125543630426310.key 1002602 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 1002707 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_3613450295733668672.key 1002707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_3613450295733668672.key 1002707 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 1002708 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1006884 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 1006901 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_3613450295733668672.key 1006902 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 1007005 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_16940742174341920595.key 1007005 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_16940742174341920595.key 1007005 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 1007006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1011317 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.31s 1011336 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_16940742174341920595.key 1011338 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 1011440 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_12026430182800705699.key 1011440 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_12026430182800705699.key 1011441 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.61ns 1011442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1015614 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 1015653 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_12026430182800705699.key 1015654 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 1015757 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_5882280899618688352.key 1015757 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_5882280899618688352.key 1015757 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 1015759 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1020146 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.39s 1020164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5882280899618688352.key 1020165 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 1020271 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 1020271 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 1020271 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 1020273 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1024642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.37s 1024660 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1024663 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 1024766 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_2092467977810734005.key 1024766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_2092467977810734005.key 1024767 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 1024767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1029019 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1029036 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_2092467977810734005.key 1029037 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 1029140 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_9163849812485488925.key 1029140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_9163849812485488925.key 1029140 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 1029141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1033391 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1033408 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_9163849812485488925.key 1033409 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 1033512 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_6992146764392519819.key 1033512 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_6992146764392519819.key 1033512 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 1033514 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1037808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s 1037826 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_6992146764392519819.key 1037828 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 1037932 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_12477244600922463506.key 1037933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_12477244600922463506.key 1037933 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 1037934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1042168 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 1042185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_12477244600922463506.key 1042187 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 1042290 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_405868255065194510.key 1042291 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_405868255065194510.key 1042291 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 1042291 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1046573 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 1046590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_405868255065194510.key 1046594 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 1046697 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_16243496633026185976.key 1046698 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_16243496633026185976.key 1046698 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.61ns 1046699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1051027 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s 1051044 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_16243496633026185976.key 1051046 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 1051151 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_14442718163219373207.key 1051152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_14442718163219373207.key 1051152 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.72ns 1051153 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1055460 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.31s 1055480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_14442718163219373207.key 1055482 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ns 1055584 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_6643831159479660144.key 1055584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_6643831159479660144.key 1055585 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 1055586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1059852 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.27s 1059869 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_6643831159479660144.key 1059871 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 1059973 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_5170630662317120263.key 1059974 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_5170630662317120263.key 1059974 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.11ns 1059975 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1064169 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s 1064186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_5170630662317120263.key 1064187 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 1064290 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_3574781488524026414.key 1064290 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_3574781488524026414.key 1064290 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 1064291 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1068539 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1068556 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_3574781488524026414.key 1068557 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 1068660 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_11559294953253082293.key 1068660 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_11559294953253082293.key 1068660 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 1068663 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1073102 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.44s 1073122 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_11559294953253082293.key 1073123 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 1073226 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_4972891720023955291.key 1073227 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_4972891720023955291.key 1073227 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.11ns 1073228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1077449 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 1077466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_4972891720023955291.key 1077468 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 1077575 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_5572931406893346879.key 1077575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_5572931406893346879.key 1077576 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 1077577 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1081842 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.27s 1081859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_5572931406893346879.key 1081860 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 1081964 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_9477766083953146625.key 1081964 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_9477766083953146625.key 1081964 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 1081965 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1086248 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 1086265 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_9477766083953146625.key 1086266 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns