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] | 4.367s | 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] | 4.361s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.405s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.415s | 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] | 4.429s | 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.409s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.433s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.445s | 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] | 4.433s | 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] | 4.390s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.471s | 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] | 4.429s | 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.381s | 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] | 4.434s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.425s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.412s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.381s | 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] | 4.408s | 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] | 4.400s | 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] | 4.368s | 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] | 4.418s | 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] | 4.378s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.396s | 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] | 4.359s | 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.356s | passed |
Standard output
982119 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 982119 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 982119 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.5ns 982119 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 986444 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s 986460 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 986475 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 986585 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_4960260920732386365.key 986585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_4960260920732386365.key 986585 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.6ns 986585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 990868 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 990884 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_4960260920732386365.key 990884 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 990993 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 990993 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 990993 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.5ns 990993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 995247 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 995263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 995278 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.7ms 995393 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_12506184897799958587.key 995393 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_12506184897799958587.key 995393 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.3ns 995393 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 999620 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 999636 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_12506184897799958587.key 999636 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 999761 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_13830640408713814081.key 999761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_13830640408713814081.key 999761 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.8ns 999761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1004051 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s 1004066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_13830640408713814081.key 1004066 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1004179 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_3290618313932472956.key 1004179 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_3290618313932472956.key 1004179 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.8ns 1004179 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1008430 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1008446 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_3290618313932472956.key 1008446 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1008557 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3443990440338942896.key 1008557 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_3443990440338942896.key 1008557 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.7ns 1008557 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1012828 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.27s 1012844 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_3443990440338942896.key 1012844 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1012953 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3951673302694530078.key 1012953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3951673302694530078.key 1012953 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.7ns 1012953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1017171 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 1017187 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_3951673302694530078.key 1017187 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1017312 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_4688769103367207582.key 1017312 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_4688769103367207582.key 1017312 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.1ns 1017312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1021543 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 1021559 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_4688769103367207582.key 1021559 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1021668 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_16072279371626362438.key 1021668 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_16072279371626362438.key 1021668 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.8ns 1021668 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1025908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 1025924 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_16072279371626362438.key 1025924 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 1026036 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 1026036 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 1026036 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.4ns 1026036 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1030272 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 1030288 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1030288 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 1030397 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_64474950457979287.key 1030397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_64474950457979287.key 1030397 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.8ns 1030397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1034661 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.27s 1034677 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_64474950457979287.key 1034677 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ns 1034802 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_2658145405605617585.key 1034802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_2658145405605617585.key 1034802 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.2ns 1034802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1039077 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 1039093 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_2658145405605617585.key 1039093 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ns 1039217 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_8797208173796187678.key 1039217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_8797208173796187678.key 1039217 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.6ns 1039217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1043517 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s 1043532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_8797208173796187678.key 1043532 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1043646 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6963761417449276167.key 1043646 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6963761417449276167.key 1043646 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225ns 1043646 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1047930 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 1047946 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_6963761417449276167.key 1047946 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1048055 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14716316051820687466.key 1048055 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14716316051820687466.key 1048055 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.9ns 1048055 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1052348 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.3s 1052364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_14716316051820687466.key 1052379 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 1052489 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_17322887462050750243.key 1052489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_17322887462050750243.key 1052489 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 253ns 1052489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1056809 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.31s 1056824 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_17322887462050750243.key 1056824 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1056934 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18110718663855488528.key 1056934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18110718663855488528.key 1056934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.3ns 1056934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1061223 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 1061254 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_18110718663855488528.key 1061254 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 1061367 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_5009902636497251129.key 1061367 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_5009902636497251129.key 1061367 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.7ns 1061367 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1065626 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.26s 1065642 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_5009902636497251129.key 1065642 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1065757 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4660222825754415755.key 1065757 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_4660222825754415755.key 1065757 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.1ns 1065757 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1070046 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s 1070061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_4660222825754415755.key 1070061 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1070186 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9633347680524934135.key 1070186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9633347680524934135.key 1070186 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.4ns 1070186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1074437 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1074452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_9633347680524934135.key 1074452 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 1074567 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_6845230325162041289.key 1074567 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_6845230325162041289.key 1074567 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.5ns 1074567 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1078876 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.31s 1078892 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_6845230325162041289.key 1078892 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.9ns 1079001 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6437216332091822162.key 1079001 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6437216332091822162.key 1079001 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.2ns 1079001 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1083298 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.3s 1083315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_6437216332091822162.key 1083315 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 1083426 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_15175656367269535013.key 1083426 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_15175656367269535013.key 1083426 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.8ns 1083426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1087698 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 1087714 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_15175656367269535013.key 1087730 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1087839 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12074127333743140522.key 1087839 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12074127333743140522.key 1087839 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.5ns 1087839 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1092091 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1092107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_12074127333743140522.key 1092107 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.1ns