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.175s | 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.077s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.096s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.047s | 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.084s | 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.060s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.214s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.172s | 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.294s | 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.111s | 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.168s | 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.067s | 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.166s | 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.099s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.061s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.142s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.137s | passed |
| [2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[2] | 3.182s | 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.139s | 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.137s | 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.091s | 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.071s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.051s | 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.065s | 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.134s | passed |
Standard output
735082 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_4964853992713856332.key 735082 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_4964853992713856332.key 735082 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 735083 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 738133 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 738146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_4964853992713856332.key 738147 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ns 738250 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 738250 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 738250 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 738251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 741312 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 741324 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 741329 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 741432 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 741432 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 741432 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 741433 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 744435 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 744449 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 744467 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.93ms 744571 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_6349695007993286618.key 744572 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_6349695007993286618.key 744572 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 744573 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 747592 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 747604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_6349695007993286618.key 747605 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ns 747708 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_9839796920430263317.key 747708 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_9839796920430263317.key 747708 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.9ns 747709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 750683 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 750695 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_9839796920430263317.key 750696 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ns 750799 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_3268464684440158501.key 750799 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_3268464684440158501.key 750799 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 750801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 753754 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 753766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_3268464684440158501.key 753767 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 753870 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_3060857352672483508.key 753870 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_3060857352672483508.key 753870 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 753871 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 756806 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 756818 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_3060857352672483508.key 756819 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 756921 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_4392366487073594425.key 756921 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_4392366487073594425.key 756921 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 756922 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 759871 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 759883 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_4392366487073594425.key 759884 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 759986 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_12018307418900704140.key 759987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_12018307418900704140.key 759987 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 759988 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 762999 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 763011 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_12018307418900704140.key 763013 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ns 763120 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_3009172665972782047.key 763120 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_3009172665972782047.key 763120 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 763121 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 766178 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 766191 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_3009172665972782047.key 766192 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 766295 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 766295 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 766296 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.1ns 766297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 769252 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 769263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 769267 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 769372 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_17508184136587904584.key 769372 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_17508184136587904584.key 769372 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 769374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 772351 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 772364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_17508184136587904584.key 772365 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 772468 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_7536044083989578464.key 772468 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_7536044083989578464.key 772468 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 772469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 775400 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 775412 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_7536044083989578464.key 775413 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 775515 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_13179976333604205873.key 775516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_13179976333604205873.key 775516 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 775516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 778474 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 778495 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_13179976333604205873.key 778496 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 778599 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_10856669070287293554.key 778599 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_10856669070287293554.key 778599 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 778600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 781543 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 781556 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_10856669070287293554.key 781557 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ns 781660 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_2982673506408973357.key 781660 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_2982673506408973357.key 781660 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 781661 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 784755 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 784767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_2982673506408973357.key 784770 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 784873 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_7776183440376142169.key 784873 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_7776183440376142169.key 784873 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 784874 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 787928 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 787941 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_7776183440376142169.key 787942 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 788045 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_14421717010970575356.key 788045 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_14421717010970575356.key 788045 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 788046 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 791223 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 791236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_14421717010970575356.key 791237 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 791339 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_10155781036910884911.key 791339 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_10155781036910884911.key 791339 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 791340 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 794333 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 794347 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_10155781036910884911.key 794348 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 794450 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_3875708975302142927.key 794451 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_3875708975302142927.key 794451 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 794451 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 797402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 797413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_3875708975302142927.key 797414 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 797517 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_14559028936189251947.key 797517 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_14559028936189251947.key 797517 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 41.6ns 797522 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 800567 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 800579 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_14559028936189251947.key 800580 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 800682 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_10445543375533084420.key 800683 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_10445543375533084420.key 800683 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 800684 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 803666 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 803678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_10445543375533084420.key 803679 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ns 803782 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_10139784856860915444.key 803782 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_10139784856860915444.key 803782 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.9ns 803783 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 806728 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 806739 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_10139784856860915444.key 806741 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ns 806845 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_11063019392881816265.key 806846 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_11063019392881816265.key 806846 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.4ns 806847 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 809872 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 809883 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_11063019392881816265.key 809885 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ns 809988 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_5260543363148994332.key 809988 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_5260543363148994332.key 809988 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.8ns 809989 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 813009 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 813020 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_5260543363148994332.key 813022 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns