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.907s | 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.911s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.812s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.820s | 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.815s | 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] | 4.128s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.815s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.884s | 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.684s | 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.738s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.835s | 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.913s | 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] | 4.383s | 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.912s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.825s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.713s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.710s | passed |
| [2] 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)[2] | 3.864s | 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.891s | 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.795s | 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.891s | 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.799s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.737s | 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.898s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 4.006s | passed |
Standard output
900128 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 900128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 900128 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.3ns 900128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 903838 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s 903853 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 903853 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.48ms 903966 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_138504469903554908.key 903966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_138504469903554908.key 903966 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.7ns 903966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 907688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 907719 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_138504469903554908.key 907719 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 907830 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 907830 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 907830 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.6ns 907830 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 911568 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 911584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 911615 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.08ms 911721 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_9529446829284800240.key 911721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_9529446829284800240.key 911721 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.9ns 911721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 915389 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 915404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_9529446829284800240.key 915404 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 915516 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_9879184905102788390.key 915516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_9879184905102788390.key 915516 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.8ns 915516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 919282 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.76s 919298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_9879184905102788390.key 919298 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 919407 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_36147149852506790.key 919407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_36147149852506790.key 919407 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.8ns 919407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 923074 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.67s 923089 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_36147149852506790.key 923089 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 923206 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3818415723789609423.key 923206 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3818415723789609423.key 923206 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.7ns 923206 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 926817 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 926833 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_3818415723789609423.key 926833 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 926943 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4391576332790297516.key 926943 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4391576332790297516.key 926943 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.7ns 926943 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 930700 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.76s 930716 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_4391576332790297516.key 930731 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.4ns 930841 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_14082793338160679589.key 930841 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_14082793338160679589.key 930841 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 525.5ns 930841 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 934705 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 934721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_14082793338160679589.key 934736 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 934847 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_3983678833177896422.key 934847 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_3983678833177896422.key 934847 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 149ns 934847 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 938614 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.77s 938645 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_3983678833177896422.key 938645 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 938755 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 938755 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 938755 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns 938755 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 942522 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.77s 942553 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 942553 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 942666 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5062562573438598231.key 942666 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5062562573438598231.key 942666 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.2ns 942666 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 946354 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.68s 946370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_5062562573438598231.key 946370 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 946479 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_4032822961334921591.key 946479 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_4032822961334921591.key 946479 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.9ns 946479 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 950174 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 950189 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_4032822961334921591.key 950189 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 950299 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_4829735875996772726.key 950299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_4829735875996772726.key 950299 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.4ns 950299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 953988 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 954004 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_4829735875996772726.key 954004 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 954114 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_13347265032362067482.key 954114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_13347265032362067482.key 954114 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.2ns 954114 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 957975 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 957990 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_13347265032362067482.key 958006 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 958242 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_12624003701210454021.key 958242 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_12624003701210454021.key 958242 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.1ns 958242 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 961932 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.68s 961947 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_12624003701210454021.key 961947 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 962058 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6906789952995367781.key 962058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6906789952995367781.key 962058 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.5ns 962058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 965801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s 965816 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_6906789952995367781.key 965833 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 965947 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_6808504046566413931.key 965947 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_6808504046566413931.key 965947 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.4ns 965947 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 969497 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 969512 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_6808504046566413931.key 969512 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 969626 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_9244773366836453262.key 969626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_9244773366836453262.key 969626 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.4ns 969626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 973238 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 973253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_9244773366836453262.key 973253 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 973364 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_17835896660703318822.key 973364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_17835896660703318822.key 973364 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 812.8ns 973364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 977149 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 977166 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_17835896660703318822.key 977166 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 977281 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_8310176565412685405.key 977281 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_8310176565412685405.key 977281 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.4ns 977281 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 981050 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.77s 981066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_8310176565412685405.key 981066 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 981666 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_4991301087039476943.key 981666 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_4991301087039476943.key 981666 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.1ns 981666 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 985446 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 985461 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_4991301087039476943.key 985461 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 985576 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_2334776808188788926.key 985576 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_2334776808188788926.key 985576 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.3ns 985576 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 989276 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s 989292 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_2334776808188788926.key 989292 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 989401 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_9695046398370652114.key 989401 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_9695046398370652114.key 989401 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 153ns 989401 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 992987 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 993003 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_9695046398370652114.key 993003 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.2ns 993117 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_17719795798944751752.key 993117 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_17719795798944751752.key 993117 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.5ns 993117 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 996698 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 996713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_17719795798944751752.key 996713 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.4ns