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.273s | 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.286s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.217s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.258s | 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.226s | 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.221s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.261s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.249s | 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.197s | 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.258s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.860s | 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.243s | 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.186s | 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.225s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.196s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.279s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.302s | 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.205s | 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.241s | 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.180s | 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.203s | 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.187s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.262s | 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.238s | 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.235s | passed |
Standard output
955662 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 955662 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 955662 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 114ns 955678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 960384 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.71s 960400 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 960415 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 960525 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1852923157617607805.key 960525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1852923157617607805.key 960525 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.7ns 960525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 964605 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 964620 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_1852923157617607805.key 964620 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 964730 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 964730 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 964730 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 353ns 964730 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 968804 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 968820 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 968867 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.72ms 968971 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3534205059638122467.key 968971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3534205059638122467.key 968971 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.9ns 968971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 973022 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s 973037 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_3534205059638122467.key 973037 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 973151 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10135300906617818000.key 973151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10135300906617818000.key 973151 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.9ns 973151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 977229 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 977245 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_10135300906617818000.key 977245 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 977354 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10225265283112276908.key 977354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10225265283112276908.key 977354 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.2ns 977354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 981411 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.06s 981427 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_10225265283112276908.key 981427 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 981541 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2310372144669236409.key 981541 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2310372144669236409.key 981541 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.2ns 981541 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 985662 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 985678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_2310372144669236409.key 985693 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.5ns 985803 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_7595748851747698088.key 985803 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_7595748851747698088.key 985803 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.2ns 985803 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 989910 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.11s 989926 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_7595748851747698088.key 989926 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 990041 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_11141189960297017313.key 990041 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_11141189960297017313.key 990041 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.7ns 990041 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 994149 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.11s 994164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_11141189960297017313.key 994164 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 994276 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_10116019567778883582.key 994276 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_10116019567778883582.key 994276 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.6ns 994276 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 998409 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 998424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_10116019567778883582.key 998440 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 998549 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 998549 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 998549 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.5ns 998549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1002706 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.16s 1002722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1002722 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 1002835 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_7222670345767479065.key 1002835 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_7222670345767479065.key 1002835 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.8ns 1002835 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1006925 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s 1006940 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_7222670345767479065.key 1006940 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1007052 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_16519986246629689236.key 1007052 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_16519986246629689236.key 1007052 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.5ns 1007052 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1011182 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 1011197 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_16519986246629689236.key 1011197 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1011310 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17905416335791427277.key 1011310 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17905416335791427277.key 1011310 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.8ns 1011310 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1015411 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 1015426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_17905416335791427277.key 1015426 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.3ns 1015536 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6320662625827529234.key 1015536 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6320662625827529234.key 1015536 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.9ns 1015536 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1019616 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s 1019631 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_6320662625827529234.key 1019647 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1019757 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16419413640747459488.key 1019757 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16419413640747459488.key 1019757 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 472.4ns 1019757 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1023878 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 1023894 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_16419413640747459488.key 1023909 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 1024019 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6316516226725274234.key 1024019 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6316516226725274234.key 1024019 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 389.6ns 1024019 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1028144 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.12s 1028160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_6316516226725274234.key 1028160 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1028269 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_11949433053273262541.key 1028269 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_11949433053273262541.key 1028269 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.4ns 1028269 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1032339 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.07s 1032354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_11949433053273262541.key 1032354 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.3ns 1032466 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6461360423430552855.key 1032466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6461360423430552855.key 1032466 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 221ns 1032466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1036582 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.12s 1036598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_6461360423430552855.key 1036613 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1036724 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11643996501027641634.key 1036724 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11643996501027641634.key 1036724 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.9ns 1036724 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1040827 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.11s 1040842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_11643996501027641634.key 1040842 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 1040967 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_2868588543468903566.key 1040967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_2868588543468903566.key 1040967 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.1ns 1040967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1045026 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.06s 1045041 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_2868588543468903566.key 1045041 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 1045153 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_7434287781116432000.key 1045153 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_7434287781116432000.key 1045153 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.5ns 1045153 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1049246 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 1049261 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_7434287781116432000.key 1049261 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1049378 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_9066730808092251626.key 1049378 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_9066730808092251626.key 1049378 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.1ns 1049378 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1053446 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.07s 1053462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_9066730808092251626.key 1053462 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1053574 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_372674480805259641.key 1053574 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_372674480805259641.key 1053574 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.3ns 1053574 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1057724 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.15s 1057740 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_372674480805259641.key 1057740 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1057853 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_629473087270415792.key 1057853 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_629473087270415792.key 1057853 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.2ns 1057853 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1062023 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 1062039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_629473087270415792.key 1062039 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns