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.162s | 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.031s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.211s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.125s | 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.048s | 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.087s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.232s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.227s | 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.097s | 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.074s | 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.209s | 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.153s | 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.148s | 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.114s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.072s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.075s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.217s | passed |
| [2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[2] | 3.053s | 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.199s | 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.193s | 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.189s | 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.085s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.072s | 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.184s | 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.180s | passed |
Standard output
718666 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl_11075747679639829833.key 718666 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl_11075747679639829833.key 718666 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.1ns 718671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 721757 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 721771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_11075747679639829833.key 721772 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 721874 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 721874 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 721874 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 721875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 724806 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 724819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 724825 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.68ms 724927 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 724928 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 724928 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 724930 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 727983 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 727996 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 728016 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.75ms 728126 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_singleton.dl_4663556107645917853.key 728126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_singleton.dl_4663556107645917853.key 728126 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 728127 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 731185 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 731207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_4663556107645917853.key 731217 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 192.9ns 731320 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_create.dl_13804272915363554833.key 731320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_create.dl_13804272915363554833.key 731320 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 731321 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 734392 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 734405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_13804272915363554833.key 734406 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 734509 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allFields.dl_8347027308892018607.key 734509 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allFields.dl_8347027308892018607.key 734509 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 734510 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 737477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 737490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_8347027308892018607.key 737491 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 737593 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqEmpty.dl_16754918285969123456.key 737594 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqEmpty.dl_16754918285969123456.key 737594 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 737594 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 740550 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 740562 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_16754918285969123456.key 740563 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 740665 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_union.dl_7674048133412936747.key 740665 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_union.dl_7674048133412936747.key 740666 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.4ns 740666 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 743731 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 743745 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_7674048133412936747.key 743747 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 743849 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl.2_4184933230355176887.key 743849 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl.2_4184933230355176887.key 743853 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.99ms 743855 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 746912 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 746926 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_4184933230355176887.key 746927 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 747030 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_wellFormed.dl_13644101712481470558.key 747030 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_wellFormed.dl_13644101712481470558.key 747030 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 747032 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 750076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 750088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_13644101712481470558.key 750089 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 750191 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 750191 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 750191 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 750192 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 753102 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 753115 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 753119 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 753222 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_empty.dl_938182250006337411.key 753223 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_empty.dl_938182250006337411.key 753223 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.5ns 753224 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 756315 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 756329 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_938182250006337411.key 756331 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 756433 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_allLocs.dl_8318399374272706245.key 756433 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_allLocs.dl_8318399374272706245.key 756434 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 917.9ns 756435 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 759442 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 759454 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_8318399374272706245.key 759456 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 759558 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_arrayRange.dl_12325824629609700400.key 759558 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_arrayRange.dl_12325824629609700400.key 759558 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 759559 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 762489 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 762502 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_12325824629609700400.key 762503 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 762606 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqConcat.dl_10027995580036773185.key 762606 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqConcat.dl_10027995580036773185.key 762606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 762607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 765575 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 765589 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_10027995580036773185.key 765591 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 765694 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqLen.dl_16831476490970843098.key 765694 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqLen.dl_16831476490970843098.key 765694 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 765695 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 768793 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 768806 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_16831476490970843098.key 768816 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 768925 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_length.dl_1559178642030833231.key 768925 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_length.dl_1559178642030833231.key 768925 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 768926 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 772034 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 772046 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_1559178642030833231.key 772050 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 772152 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_freshLocs.dl_11065582792347136781.key 772152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_freshLocs.dl_11065582792347136781.key 772152 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 772153 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 775133 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 775146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_11065582792347136781.key 775147 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.3ns 775249 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_anon.dl_4195770700929956385.key 775249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_anon.dl_4195770700929956385.key 775249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 775250 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 778203 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 778219 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_4195770700929956385.key 778221 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 778324 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_memset.dl_3941021482304315319.key 778324 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_memset.dl_3941021482304315319.key 778324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 778325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 781360 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 781372 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_3941021482304315319.key 781373 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 781476 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_store.dl_3295091881627736062.key 781477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_store.dl_3295091881627736062.key 781477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 781478 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 784509 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 784521 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_3295091881627736062.key 784522 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 784624 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSub.dl.2_9917254663827850502.key 784625 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSub.dl.2_9917254663827850502.key 784625 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 784626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 787621 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 787634 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_9917254663827850502.key 787635 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.6ns 787738 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl_2418861613001348706.key 787738 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl_2418861613001348706.key 787738 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 787739 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 790693 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 790706 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_2418861613001348706.key 790707 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 790810 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_seqSingleton.dl.2_8421762031403393004.key 790810 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_seqSingleton.dl.2_8421762031403393004.key 790810 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 790811 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 793765 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 793780 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_8421762031403393004.key 793782 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 793885 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file /tmp/SMT_lemma_null.dl_13768823830395889903.key 793885 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/SMT_lemma_null.dl_13768823830395889903.key 793885 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.4ns 793892 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 796984 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 796998 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_13768823830395889903.key 797000 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns