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] | 2.682s | 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.099s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.743s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.823s | 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] | 2.718s | 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] | 2.709s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.711s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.769s | 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] | 2.771s | 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] | 2.800s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.854s | 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] | 2.688s | 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] | 2.702s | 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] | 2.736s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.746s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.848s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.685s | 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] | 2.747s | 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] | 2.766s | 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] | 2.800s | 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] | 2.814s | 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] | 2.731s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.798s | 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] | 2.721s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 2.695s | passed |
Standard output
651812 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 651812 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 651812 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.1ns 651830 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 654549 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 654565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 654565 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.23ms 654678 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10496521305382246418.key 654678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10496521305382246418.key 654678 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.6ns 654678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 657287 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 657302 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_10496521305382246418.key 657302 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 657412 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 657412 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 657412 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.6ns 657412 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 660019 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 660035 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 660066 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.62ms 660178 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_13613483184677360847.key 660178 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_13613483184677360847.key 660178 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.9ns 660178 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 662835 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 662867 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_13613483184677360847.key 662867 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 662979 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14847248513488227075.key 662979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14847248513488227075.key 662979 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.3ns 662979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 665654 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 665670 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_14847248513488227075.key 665685 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 665795 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_4678299750445975406.key 665795 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_4678299750445975406.key 665795 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.9ns 665795 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 668394 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 668409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_4678299750445975406.key 668409 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ns 668526 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8452567192657958886.key 668526 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8452567192657958886.key 668526 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.6ns 668526 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 671195 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 671211 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_8452567192657958886.key 671211 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 671325 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6666849052764926320.key 671325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6666849052764926320.key 671325 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.6ns 671325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 673906 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 673921 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_6666849052764926320.key 673921 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 674046 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_968951475246394679.key 674046 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_968951475246394679.key 674046 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.7ns 674046 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 676610 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 676626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_968951475246394679.key 676626 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 676742 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_3216955489451323154.key 676742 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_3216955489451323154.key 676742 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.1ns 676742 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 679292 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 679308 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_3216955489451323154.key 679308 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 679424 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 679424 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 679424 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.6ns 679424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 682128 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 682144 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 682410 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 252.67ms 682523 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_13217158726864838703.key 682523 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_13217158726864838703.key 682523 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 126ns 682523 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 685142 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 685158 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_13217158726864838703.key 685158 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 685267 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_14080659517990238429.key 685267 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_14080659517990238429.key 685267 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.9ns 685267 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 687949 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 687965 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_14080659517990238429.key 687965 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 688090 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_6761942131174520105.key 688090 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_6761942131174520105.key 688090 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.6ns 688090 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 690680 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 690695 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_6761942131174520105.key 690695 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 690808 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_7471419419608003487.key 690808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_7471419419608003487.key 690808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.1ns 690808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 693388 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 693404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_7471419419608003487.key 693404 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 693517 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_12499643758324385463.key 693517 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_12499643758324385463.key 693517 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.8ns 693517 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 696097 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 696113 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_12499643758324385463.key 696113 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 696229 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15136645088353511478.key 696229 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15136645088353511478.key 696229 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.2ns 696229 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 698872 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 698887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_15136645088353511478.key 698887 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 698998 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_11851215675698881330.key 698998 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_11851215675698881330.key 698998 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.2ns 698998 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 701647 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 701663 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_11851215675698881330.key 701663 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 701772 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_18017045559676546210.key 701772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_18017045559676546210.key 701772 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.3ns 701772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 704445 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 704461 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_18017045559676546210.key 704461 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 704570 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_8799583222236987143.key 704570 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_8799583222236987143.key 704570 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.6ns 704570 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 707118 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 707134 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_8799583222236987143.key 707134 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 707259 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5933235824924723709.key 707259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5933235824924723709.key 707259 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.7ns 707259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 709832 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 709847 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_5933235824924723709.key 709847 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 709961 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_18021579551758749406.key 709961 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_18021579551758749406.key 709961 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 515.8ns 709961 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 712556 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 712572 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_18021579551758749406.key 712572 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 712697 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_18299647512425389651.key 712697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_18299647512425389651.key 712697 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.9ns 712697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 715308 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 715324 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_18299647512425389651.key 715339 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 715450 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_15433832389978609878.key 715450 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_15433832389978609878.key 715450 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.2ns 715450 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 718171 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 718186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_15433832389978609878.key 718186 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 718296 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12025946018442819416.key 718296 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12025946018442819416.key 718296 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.3ns 718296 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 720859 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 720875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_12025946018442819416.key 720875 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.3ns