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.414s | 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.269s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.354s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.206s | 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.486s | passed |
| [15] seqConcat.dl, \forall int i; \forall Seq s1; \forall Seq s2; ( 0 <= i & i < seqLen(s1) + seqLen(s2) -> any::seqGet(seqConcat(s1, s2), i) = \if (i < seqLen(s1)) \then (any::seqGet(s1, i)) \else (any::seqGet(s2, i-seqLen(s1)))) | testSMTLemmaSoundness(String, String)[15] | 3.359s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.436s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.254s | 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.221s | 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.221s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.323s | 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.340s | passed |
| [21] store.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; \forall any v; any::select(store(h,o,f,v), o2, f2)<<Trigger>> = \if(o = o2 & f = f2 & f != java.lang.Object::<created>) \then(v) \else(any::select(h, o2, f2)) | testSMTLemmaSoundness(String, String)[21] | 3.395s | 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.274s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.346s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.355s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.412s | 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.396s | 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.477s | 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.132s | 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.213s | 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.236s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.273s | 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.530s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 3.462s | passed |
Standard output
794639 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 794639 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 794639 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns 794639 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 797827 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 797843 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 797859 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.81ms 797969 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_2671554803708149914.key 797969 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_2671554803708149914.key 797969 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.3ns 797969 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 801240 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 801256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_2671554803708149914.key 801256 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 801365 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 801365 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 801365 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.1ns 801365 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 804499 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 804530 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 804732 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 189.98ms 804842 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_6219495766664306551.key 804842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_6219495766664306551.key 804842 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.3ns 804842 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 807849 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 807864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_6219495766664306551.key 807864 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 807974 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_6468817100943719060.key 807974 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_6468817100943719060.key 807974 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 403.8ns 807974 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 811056 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 811072 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_6468817100943719060.key 811072 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 811187 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_18264214517705822301.key 811187 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_18264214517705822301.key 811187 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.3ns 811187 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 814298 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 814298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_18264214517705822301.key 814313 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 814423 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8526883896851040023.key 814423 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8526883896851040023.key 814423 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.1ns 814423 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 817559 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 817575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_8526883896851040023.key 817575 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 817696 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15832093206872680386.key 817696 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15832093206872680386.key 817696 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.9ns 817696 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 820999 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 821015 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_15832093206872680386.key 821015 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 821226 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_7307075645057326667.key 821226 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_7307075645057326667.key 821226 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.8ns 821226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 824557 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 824572 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_7307075645057326667.key 824572 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 824688 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_3694067411819670189.key 824688 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_3694067411819670189.key 824688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.3ns 824688 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 827976 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 827991 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_3694067411819670189.key 827991 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.3ns 828102 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 828102 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 828102 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.9ns 828102 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 831230 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 831246 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 831261 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.07ms 831371 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11115416955619508354.key 831371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11115416955619508354.key 831371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 518.9ns 831371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 834594 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 834610 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_11115416955619508354.key 834610 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 834725 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_555763096275116080.key 834725 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_555763096275116080.key 834725 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.2ns 834725 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 837806 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 837806 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_555763096275116080.key 837822 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 837931 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_13203877664042175592.key 837931 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_13203877664042175592.key 837931 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.6ns 837931 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 841292 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 841308 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_13203877664042175592.key 841308 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 841417 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11748586109950299302.key 841417 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11748586109950299302.key 841417 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.8ns 841433 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 844649 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 844664 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_11748586109950299302.key 844664 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 844776 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10188976869303831097.key 844776 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10188976869303831097.key 844776 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.7ns 844776 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 848087 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 848087 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_10188976869303831097.key 848103 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 848212 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6923417765248628165.key 848212 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6923417765248628165.key 848212 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.9ns 848212 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 851335 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 851351 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_6923417765248628165.key 851351 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 851466 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2259031596383638629.key 851466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2259031596383638629.key 851466 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.8ns 851466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 854562 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 854578 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_2259031596383638629.key 854578 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 854687 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_14932864600205157684.key 854687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_14932864600205157684.key 854687 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.8ns 854687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 857783 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 857799 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_14932864600205157684.key 857799 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 857908 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_10233292525239445257.key 857908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_10233292525239445257.key 857908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 409.2ns 857908 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 861117 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 861132 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_10233292525239445257.key 861132 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 861248 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5458064149841690189.key 861248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5458064149841690189.key 861248 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.9ns 861248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 864502 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 864534 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_5458064149841690189.key 864534 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 864643 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_8280729142834740456.key 864643 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_8280729142834740456.key 864643 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.9ns 864643 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 867792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 867807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_8280729142834740456.key 867807 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 867917 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_18398313938362524745.key 867917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_18398313938362524745.key 867917 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.8ns 867917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 871130 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 871145 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_18398313938362524745.key 871145 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 871263 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_10867870506270843340.key 871263 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_10867870506270843340.key 871263 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.3ns 871263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 874492 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 874507 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_10867870506270843340.key 874507 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 874619 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_14444594500484263054.key 874619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_14444594500484263054.key 874619 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.4ns 874619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 877902 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 877918 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_14444594500484263054.key 877918 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.2ns