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] | 3.168s | 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] | 3.238s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.175s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.148s | 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] | 3.158s | 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] | 3.273s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.188s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.353s | 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] | 3.278s | 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] | 3.332s | 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] | 3.088s | 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] | 3.435s | 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] | 3.234s | 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] | 3.209s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.008s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.146s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.069s | passed |
| [2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[2] | 3.149s | 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] | 3.187s | 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] | 3.096s | passed |
| [5] 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)[5] | 3.305s | passed |
| [6] allFields.dl, \forall Object o; \forall Field f; \forall Object o2; ( elementOf(o,f, allFields(o2))<<Trigger>> <-> o = o2 ) | testSMTLemmaSoundness(String, String)[6] | 3.058s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.211s | 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] | 3.051s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 3.116s | passed |
Standard output
726494 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_7961659802243030897.key 726494 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_7961659802243030897.key 726494 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 726495 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 729457 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 729476 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_7961659802243030897.key 729478 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 729581 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 729581 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 729581 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 729584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 732607 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 732622 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 732627 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 732730 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 732731 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 732732 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.01ns 732733 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 735786 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 735802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 735814 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ms 735918 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_13799145798128139918.key 735918 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_13799145798128139918.key 735919 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 735920 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 738885 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 738907 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_13799145798128139918.key 738911 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 739013 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_7131489074078656310.key 739013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_7131489074078656310.key 739014 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.3ns 739015 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 742199 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 742214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_7131489074078656310.key 742215 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ns 742319 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_15831468285170923773.key 742320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_15831468285170923773.key 742321 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.11ns 742322 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 745258 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 745273 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_15831468285170923773.key 745274 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 745377 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_15586642244760732257.key 745378 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_15586642244760732257.key 745378 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.01ns 745379 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 748465 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 748483 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_15586642244760732257.key 748485 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 748587 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_8410555555193710284.key 748587 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_8410555555193710284.key 748587 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 748588 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 751520 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 751535 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_8410555555193710284.key 751536 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ns 751639 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_12363779305199875226.key 751639 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_12363779305199875226.key 751639 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 751640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 754633 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 754650 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_12363779305199875226.key 754651 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 754754 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_5590348468796046512.key 754755 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_5590348468796046512.key 754756 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.71ns 754760 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 757801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 757817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5590348468796046512.key 757819 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 757921 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 757922 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 757922 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 757923 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 761033 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 761051 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 761055 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.74ms 761162 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_5735757818279787549.key 761163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_5735757818279787549.key 761164 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.61ns 761165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 764213 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 764229 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_5735757818279787549.key 764234 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 764336 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_5530877966655214048.key 764337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_5530877966655214048.key 764337 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 764340 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 767366 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 767381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_5530877966655214048.key 767382 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ns 767484 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_415333103260843553.key 767485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_415333103260843553.key 767485 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.81ns 767486 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 770500 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 770532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_415333103260843553.key 770538 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 770644 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_14334329402759627454.key 770644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_14334329402759627454.key 770644 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 770645 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 773795 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 773811 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_14334329402759627454.key 773812 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 773916 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_16116410357031053545.key 773916 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_16116410357031053545.key 773916 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 773917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 776980 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 776999 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_16116410357031053545.key 777000 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 777103 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_11897943341073416832.key 777103 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_11897943341073416832.key 777103 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 777104 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 780333 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 780348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_11897943341073416832.key 780350 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 780456 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_5395089196024351878.key 780457 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_5395089196024351878.key 780458 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.11ns 780459 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 783613 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 783630 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_5395089196024351878.key 783632 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 783734 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_15614567523671642356.key 783734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_15614567523671642356.key 783734 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.1ns 783736 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 786943 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 786962 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_15614567523671642356.key 786963 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 787066 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_16324076614009147171.key 787066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_16324076614009147171.key 787066 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 787068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 790379 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 790395 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_16324076614009147171.key 790396 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 790501 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_8471117607122269232.key 790501 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_8471117607122269232.key 790501 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.41ns 790503 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 793615 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 793632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_8471117607122269232.key 793633 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 793735 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_17605031657023270715.key 793735 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_17605031657023270715.key 793735 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 793736 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 796821 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 796836 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_17605031657023270715.key 796837 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 796944 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_13794336305027061339.key 796945 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_13794336305027061339.key 796945 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 796946 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 799834 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 799849 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_13794336305027061339.key 799850 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 799953 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_1926688777655745519.key 799953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_1926688777655745519.key 799953 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 799954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 802976 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 802993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_1926688777655745519.key 802995 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 803099 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_5836732474825420083.key 803099 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_5836732474825420083.key 803100 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.01ns 803101 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 806049 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 806064 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_5836732474825420083.key 806065 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns