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.752s | 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.605s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.571s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.480s | 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.621s | 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.455s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.797s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.635s | 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.434s | 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.376s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.462s | 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.258s | 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.416s | 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.722s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.705s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.596s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.523s | 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.449s | 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.669s | 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.588s | 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.367s | 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.444s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.418s | 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.454s | 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.494s | passed |
Standard output
842551 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 842551 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 842551 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns 842567 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 845872 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 845888 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 845888 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.78ms 846013 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_6413663697263562346.key 846013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_6413663697263562346.key 846013 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243ns 846013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 849330 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 849346 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_6413663697263562346.key 849346 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 849462 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 849462 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 849462 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.2ns 849462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 852923 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 852939 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 853017 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.07ms 853131 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_8725336042692721118.key 853131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_8725336042692721118.key 853131 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.9ns 853131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 856594 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 856609 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_8725336042692721118.key 856609 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 856721 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14025804505731886562.key 856721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14025804505731886562.key 856721 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.9ns 856721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 859963 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 859979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_14025804505731886562.key 859979 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 860088 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12432159429937795752.key 860088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12432159429937795752.key 860088 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.6ns 860088 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 863403 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 863419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_12432159429937795752.key 863419 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 863532 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_4491576573018407965.key 863532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_4491576573018407965.key 863532 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.4ns 863532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 866810 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 866825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_4491576573018407965.key 866841 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.1ns 866950 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3323181967142892203.key 866950 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3323181967142892203.key 866950 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.5ns 866950 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 870279 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 870295 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_3323181967142892203.key 870295 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 870404 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_1471258919427262408.key 870404 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_1471258919427262408.key 870404 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 269ns 870404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 873757 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 873773 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_1471258919427262408.key 873789 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 873898 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6195927016428636674.key 873898 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6195927016428636674.key 873898 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.1ns 873898 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 877510 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 877525 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_6195927016428636674.key 877541 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 877650 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 877713 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 877728 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.2ns 877760 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 881127 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 881143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 881143 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 881255 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_8245353996724135434.key 881255 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_8245353996724135434.key 881255 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 146ns 881255 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 884685 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 884701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_8245353996724135434.key 884717 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 884827 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_3550635384867318800.key 884827 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_3550635384867318800.key 884827 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.1ns 884827 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 888182 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 888197 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_3550635384867318800.key 888197 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 888307 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_355878948257955249.key 888307 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_355878948257955249.key 888307 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.8ns 888307 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 891796 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 891812 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_355878948257955249.key 891812 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 891928 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6246805484172652679.key 891928 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_6246805484172652679.key 891928 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.2ns 891928 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 895243 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 895258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_6246805484172652679.key 895274 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 895383 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13611955504439942448.key 895383 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13611955504439942448.key 895383 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.9ns 895383 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 899009 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s 899025 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_13611955504439942448.key 899056 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 899181 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_3368239465214874845.key 899181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_3368239465214874845.key 899181 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 433.7ns 899181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 902687 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 902703 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_3368239465214874845.key 902703 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.1ns 902817 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_12790538627707978969.key 902817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_12790538627707978969.key 902817 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.58ms 902817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 906110 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 906141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_12790538627707978969.key 906141 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.3ns 906251 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_18124852140124979933.key 906251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_18124852140124979933.key 906251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.2ns 906251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 909505 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 909521 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_18124852140124979933.key 909521 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 909627 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_12378483785066997160.key 909627 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_12378483785066997160.key 909627 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 454.5ns 909627 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 912754 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 912770 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_12378483785066997160.key 912770 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 912885 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_12984508433501094432.key 912885 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_12984508433501094432.key 912885 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.8ns 912885 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 916161 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 916176 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_12984508433501094432.key 916192 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 916301 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_7682161994846320408.key 916301 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_7682161994846320408.key 916301 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.4ns 916301 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 919881 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 919912 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_7682161994846320408.key 919912 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 920023 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_9842039047763378563.key 920023 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_9842039047763378563.key 920023 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.1ns 920023 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 923587 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 923603 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_9842039047763378563.key 923603 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 923728 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_971355985116627618.key 923728 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_971355985116627618.key 923728 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.8ns 923728 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 927199 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 927215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_971355985116627618.key 927215 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 927325 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_8689246696106493168.key 927325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_8689246696106493168.key 927325 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.8ns 927325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 930718 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 930734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_8689246696106493168.key 930734 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns