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.173s | 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.199s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.168s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.180s | 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.160s | 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.133s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.174s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.177s | 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.144s | 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.125s | 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.379s | 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.166s | 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.185s | 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.180s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.149s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.149s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.170s | passed |
| [2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[2] | 3.288s | 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.302s | 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.212s | 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.219s | 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.214s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.132s | 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.207s | 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.204s | passed |
Standard output
740225 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_16611840995771664313.key 740226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_16611840995771664313.key 740226 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 740226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 743482 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 743498 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_16611840995771664313.key 743499 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 743602 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 743602 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 743602 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 743603 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 746765 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 746780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 746786 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 746890 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 746890 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 746890 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 746891 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 750050 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 750064 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 750086 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.42ms 750191 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_16979947906337902389.key 750191 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_16979947906337902389.key 750191 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 750193 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 753285 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 753300 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_16979947906337902389.key 753301 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 753404 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_1812038015936350120.key 753405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_1812038015936350120.key 753405 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 753406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 756503 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 756518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_1812038015936350120.key 756519 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 756622 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_6655376927243714500.key 756622 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_6655376927243714500.key 756622 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 756624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 759715 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 759732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_6655376927243714500.key 759734 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 759836 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_9882168791019930000.key 759836 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_9882168791019930000.key 759836 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 759837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 762850 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 762865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_9882168791019930000.key 762866 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 762969 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_4570115979598447995.key 762969 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_4570115979598447995.key 762969 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 762970 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 766056 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 766071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_4570115979598447995.key 766073 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 766175 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_8380043130796291401.key 766175 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_8380043130796291401.key 766175 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 766176 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 769261 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 769276 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_8380043130796291401.key 769277 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 769379 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_13836505423089190195.key 769380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_13836505423089190195.key 769380 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 769381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 772433 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 772448 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_13836505423089190195.key 772449 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 772551 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 772552 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 772552 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 772553 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 775629 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 775643 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 775648 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 775751 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_15623780389758591063.key 775751 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_15623780389758591063.key 775751 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 775752 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 778801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 778816 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_15623780389758591063.key 778817 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 778919 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_7748986929896362444.key 778920 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_7748986929896362444.key 778920 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 778922 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 781979 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 781994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_7748986929896362444.key 781996 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 782099 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_10706089410937291974.key 782099 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_10706089410937291974.key 782099 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 782100 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 785139 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 785155 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_10706089410937291974.key 785156 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 785259 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_15639649428967081335.key 785259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_15639649428967081335.key 785259 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 785260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 788273 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 788289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_15639649428967081335.key 788290 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 788393 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_13446484108727756828.key 788395 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_13446484108727756828.key 788395 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.11ns 788396 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 791447 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 791461 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_13446484108727756828.key 791462 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 791566 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_8467727317818747911.key 791567 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_8467727317818747911.key 791567 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 791567 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 794626 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 794640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_8467727317818747911.key 794641 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 794743 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_15724469245718045715.key 794744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_15724469245718045715.key 794744 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 794745 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 797746 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 797783 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_15724469245718045715.key 797784 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ns 797887 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_7913836156113512773.key 797887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_7913836156113512773.key 797887 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 797888 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 800891 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 800907 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_7913836156113512773.key 800908 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 801013 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_16092745733220714330.key 801014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_16092745733220714330.key 801014 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.71ns 801015 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 804060 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 804075 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_16092745733220714330.key 804076 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 804178 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_3348471431008911536.key 804178 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_3348471431008911536.key 804178 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 804179 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 807245 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 807260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_3348471431008911536.key 807261 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 807363 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_6717977881770455634.key 807364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_6717977881770455634.key 807364 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 807365 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 810425 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 810440 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_6717977881770455634.key 810441 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 810543 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_6468563275943793811.key 810544 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_6468563275943793811.key 810544 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 810544 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 813572 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 813588 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_6468563275943793811.key 813589 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 813692 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_10731574712342417251.key 813692 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_10731574712342417251.key 813692 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 813693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 816723 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 816737 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_10731574712342417251.key 816738 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 816841 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_46913939689121993.key 816841 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_46913939689121993.key 816841 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 816842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 819893 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 819908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_46913939689121993.key 819909 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns