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.708s | 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.688s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.597s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.440s | 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.456s | 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.361s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.438s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.579s | 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.519s | 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.471s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.644s | 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.469s | 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.394s | 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.408s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.579s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.611s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.830s | 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.574s | 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.658s | 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.534s | 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.580s | 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.611s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.579s | 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.518s | 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.393s | passed |
Standard output
859184 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 859184 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 859184 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.1ns 859184 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 862687 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 862702 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 862718 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 862827 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_5995791204621395554.key 862843 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_5995791204621395554.key 862843 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.3ns 862843 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 866283 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 866298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_5995791204621395554.key 866298 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 866408 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 866408 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 866408 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.9ns 866408 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 869894 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 869910 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 869956 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.65ms 870066 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_9520134454047210846.key 870066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_9520134454047210846.key 870066 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.9ns 870066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 873476 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 873491 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_9520134454047210846.key 873491 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 873601 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12283206786831029183.key 873601 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12283206786831029183.key 873601 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.2ns 873601 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 877040 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 877056 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_12283206786831029183.key 877072 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 877181 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8892051724708816827.key 877181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8892051724708816827.key 877181 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.9ns 877181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 880667 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 880683 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_8892051724708816827.key 880683 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.9ns 880792 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17775083761321766103.key 880792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17775083761321766103.key 880792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.5ns 880792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 884247 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 884263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_17775083761321766103.key 884263 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 884372 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_2141989935082000840.key 884372 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_2141989935082000840.key 884372 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.2ns 884372 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 887750 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 887781 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_2141989935082000840.key 887781 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 887890 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_1050982275670559798.key 887890 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_1050982275670559798.key 887890 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.9ns 887890 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 891142 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 891158 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_1050982275670559798.key 891174 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 891283 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_15586356688726049620.key 891283 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_15586356688726049620.key 891283 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.2ns 891283 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 894850 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 894866 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_15586356688726049620.key 894881 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 894991 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 894991 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 894991 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.1ns 894991 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 898555 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 898570 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 898570 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 898680 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_7081102850575741840.key 898680 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_7081102850575741840.key 898680 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.3ns 898680 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 902152 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 902168 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_7081102850575741840.key 902168 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 902277 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_17788550740505184753.key 902277 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_17788550740505184753.key 902277 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 285ns 902277 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 905592 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 905607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_17788550740505184753.key 905607 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 905717 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17509608436972116825.key 905717 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17509608436972116825.key 905717 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.5ns 905717 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 909032 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 909047 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_17509608436972116825.key 909063 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 909173 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6293825328934985474.key 909173 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6293825328934985474.key 909173 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 339ns 909173 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 912409 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 912425 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_6293825328934985474.key 912425 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 912534 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9985194637089787039.key 912534 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9985194637089787039.key 912534 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.9ns 912534 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 915849 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 915865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_9985194637089787039.key 915865 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 915975 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_16474929473221378867.key 915975 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_16474929473221378867.key 915975 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.4ns 915975 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 919429 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 919445 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_16474929473221378867.key 919445 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 919554 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2211045174226440990.key 919554 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2211045174226440990.key 919554 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.7ns 919554 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 922948 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 922964 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_2211045174226440990.key 922964 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 923073 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_312779337591230138.key 923073 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_312779337591230138.key 923073 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.3ns 923073 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 926419 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 926434 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_312779337591230138.key 926434 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 926544 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_6862021935919924734.key 926544 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_6862021935919924734.key 926544 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 513.3ns 926544 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 929889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 929904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_6862021935919924734.key 929904 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 930014 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_471698172317772939.key 930014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_471698172317772939.key 930014 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.5ns 930014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 933283 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 933299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_471698172317772939.key 933299 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 933408 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_3141292349779577383.key 933408 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_3141292349779577383.key 933408 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 447.5ns 933408 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 936691 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 936707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_3141292349779577383.key 936707 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 936817 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12191387820534970487.key 936817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12191387820534970487.key 936817 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 502.3ns 936817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 940255 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 940271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_12191387820534970487.key 940287 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 940396 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_6989114996544308796.key 940396 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_6989114996544308796.key 940396 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.1ns 940396 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 943883 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 943899 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_6989114996544308796.key 943899 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 944008 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_2016090834319760601.key 944008 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_2016090834319760601.key 944008 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.4ns 944008 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 947698 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 947713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_2016090834319760601.key 947729 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns