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.571s | 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.472s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.662s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.436s | 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.498s | 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.662s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.448s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.534s | 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.728s | 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.405s | 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.525s | 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.648s | 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.963s | 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.369s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.530s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.600s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.355s | passed |
| [2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[2] | 3.345s | 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.586s | 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.390s | 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.302s | 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.463s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.398s | 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.328s | 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.571s | passed |
Standard output
806765 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_4210122106064611601.key 806766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_4210122106064611601.key 806766 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.9ns 806767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 810168 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 810185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_4210122106064611601.key 810186 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 810289 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 810289 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 810289 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 810290 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 813507 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 813523 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 813531 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.1ms 813635 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 813635 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 813635 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 813638 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 817045 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 817061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 817111 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.17ms 817221 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_7661331575919960781.key 817221 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_7661331575919960781.key 817222 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.1ns 817223 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 820486 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 820506 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_7661331575919960781.key 820507 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 820610 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_8230376218646136565.key 820610 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_8230376218646136565.key 820610 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.9ns 820611 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 823788 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 823805 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_8230376218646136565.key 823810 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.3ns 823912 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_9767988157166263587.key 823913 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_9767988157166263587.key 823913 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 823914 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 827235 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 827264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_9767988157166263587.key 827265 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 827375 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_15063964720330687949.key 827376 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_15063964720330687949.key 827376 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 827376 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 830655 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 830669 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_15063964720330687949.key 830670 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 830774 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_11642652191872652139.key 830774 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_11642652191872652139.key 830774 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.1ns 830775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 833979 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 833998 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_11642652191872652139.key 834000 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 834103 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_4406876884119393053.key 834104 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_4406876884119393053.key 834104 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 422ns 834106 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 837553 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 837569 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_4406876884119393053.key 837570 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 837673 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_18136804757101852516.key 837674 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_18136804757101852516.key 837674 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 837677 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 841124 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 841140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_18136804757101852516.key 841142 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 841244 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 841244 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 841244 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 841245 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 844573 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 844591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 844612 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.73ms 844716 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_4864857751947997958.key 844716 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_4864857751947997958.key 844716 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.9ns 844717 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 848248 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 848273 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_4864857751947997958.key 848275 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 848380 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_4536005315668856616.key 848380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_4536005315668856616.key 848380 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.7ns 848383 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 851696 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 851712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_4536005315668856616.key 851713 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 851815 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_2074135740151596216.key 851816 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_2074135740151596216.key 851816 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 851817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 855188 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 855208 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_2074135740151596216.key 855210 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 855313 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_3117053395821033202.key 855320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_3117053395821033202.key 855320 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 855321 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 858849 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 858864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_3117053395821033202.key 858866 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 858976 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_6417021875095366130.key 858977 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_6417021875095366130.key 858977 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 858981 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 862304 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 862319 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_6417021875095366130.key 862320 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 862424 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_13265913731067149774.key 862424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_13265913731067149774.key 862424 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 862425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 865834 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 865853 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_13265913731067149774.key 865855 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 865957 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_7522796738696753546.key 865958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_7522796738696753546.key 865958 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 865963 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 869563 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 869580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_7522796738696753546.key 869582 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 869685 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_7658355898634163201.key 869685 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_7658355898634163201.key 869685 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.7ns 869687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 872970 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 872986 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_7658355898634163201.key 872987 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 873090 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_4305400385934199319.key 873091 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_4305400385934199319.key 873091 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 873092 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 876616 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 876634 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_4305400385934199319.key 876635 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 876738 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_7887872676547766337.key 876738 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_7887872676547766337.key 876738 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 876739 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 880581 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.84s 880597 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_7887872676547766337.key 880598 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 880701 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_3186177812443742316.key 880702 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_3186177812443742316.key 880702 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 880703 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 883951 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 883966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_3186177812443742316.key 883968 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 884070 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_8924996933048899923.key 884071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_8924996933048899923.key 884071 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 884072 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 887478 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 887495 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_8924996933048899923.key 887496 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 887600 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_17292516618505532480.key 887600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_17292516618505532480.key 887600 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 887605 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 891082 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 891096 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_17292516618505532480.key 891098 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 891204 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_10966696643954674252.key 891204 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_10966696643954674252.key 891204 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 891206 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 894439 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 894455 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_10966696643954674252.key 894456 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns