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.238s | 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.246s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.249s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.224s | 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.229s | 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.248s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.227s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.182s | 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.180s | 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.185s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.312s | 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.219s | 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.182s | 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.173s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.184s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.167s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.172s | 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.309s | 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.301s | 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.215s | 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.198s | 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.209s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.223s | 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.203s | 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.249s | passed |
Standard output
954989 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 954989 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 954989 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.3ns 954991 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 959158 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 959174 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 959174 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.85ms 959299 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_18385830606780043427.key 959299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_18385830606780043427.key 959299 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.5ns 959299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 963467 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 963483 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_18385830606780043427.key 963483 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 963608 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 963608 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 963608 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.5ns 963608 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 967753 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 967768 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 967800 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.51ms 967909 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_14679429587580454047.key 967909 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_14679429587580454047.key 967909 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.6ns 967909 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 971997 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s 972012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_14679429587580454047.key 972012 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 972124 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_16202673434186004481.key 972124 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_16202673434186004481.key 972124 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.4ns 972124 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 976194 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.07s 976210 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_16202673434186004481.key 976210 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 976322 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_4454866954325378194.key 976322 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_4454866954325378194.key 976322 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.1ns 976322 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 980402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 980418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_4454866954325378194.key 980418 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 980532 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_16358831252651101511.key 980532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_16358831252651101511.key 980532 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247ns 980532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 984626 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 984642 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_16358831252651101511.key 984642 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 984755 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_9361429110672441817.key 984755 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_9361429110672441817.key 984755 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.5ns 984755 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 988828 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 988844 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_9361429110672441817.key 988844 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 988958 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_9671305762815593134.key 988958 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_9671305762815593134.key 988958 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.9ns 988958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 993080 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.12s 993095 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_9671305762815593134.key 993095 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 993208 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_7793568816562866630.key 993208 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_7793568816562866630.key 993208 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.9ns 993208 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 997320 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.11s 997335 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_7793568816562866630.key 997335 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.7ns 997446 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 997446 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 997446 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.7ns 997446 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1001551 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.11s 1001567 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1001567 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 1001692 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_13942349936389761053.key 1001692 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_13942349936389761053.key 1001692 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.5ns 1001692 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1005816 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.12s 1005831 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_13942349936389761053.key 1005831 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 1005941 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_1979903291574091786.key 1005941 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_1979903291574091786.key 1005941 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.4ns 1005941 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1010024 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s 1010040 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_1979903291574091786.key 1010040 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.4ns 1010165 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11680837226856962944.key 1010165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11680837226856962944.key 1010165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.3ns 1010165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1014263 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 1014278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_11680837226856962944.key 1014278 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1014394 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15190753185205533050.key 1014394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15190753185205533050.key 1014394 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.2ns 1014394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1018517 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.12s 1018532 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_15190753185205533050.key 1018532 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 1018642 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9088358110552682456.key 1018642 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9088358110552682456.key 1018642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.4ns 1018642 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1022745 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 1022760 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_9088358110552682456.key 1022760 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.8ns 1022870 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15581871895635488585.key 1022870 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15581871895635488585.key 1022870 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.7ns 1022870 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1026922 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s 1026938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_15581871895635488585.key 1026938 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1027052 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_8790668722284982260.key 1027052 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_8790668722284982260.key 1027052 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.6ns 1027052 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1031102 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s 1031118 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_8790668722284982260.key 1031118 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ns 1031232 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_16302843977790614211.key 1031232 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_16302843977790614211.key 1031232 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.5ns 1031232 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1035290 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.06s 1035305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_16302843977790614211.key 1035305 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.7ns 1035417 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_6852848878758332928.key 1035417 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_6852848878758332928.key 1035417 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.6ns 1035417 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1039497 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s 1039527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_6852848878758332928.key 1039527 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.4ns 1039637 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9812546679319809119.key 1039637 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9812546679319809119.key 1039637 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239ns 1039637 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1043692 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s 1043708 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_9812546679319809119.key 1043708 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.9ns 1043819 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_12243624544101357684.key 1043819 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_12243624544101357684.key 1043819 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.4ns 1043819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1047851 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s 1047867 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_12243624544101357684.key 1047883 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1047992 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3710645417354200270.key 1047992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3710645417354200270.key 1047992 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.6ns 1047992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1052035 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s 1052051 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_3710645417354200270.key 1052066 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.7ns 1052176 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_3755133222866685363.key 1052176 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_3755133222866685363.key 1052176 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.1ns 1052176 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1056218 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s 1056234 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_3755133222866685363.key 1056234 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1056343 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_10791935800163803658.key 1056343 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_10791935800163803658.key 1056343 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.5ns 1056343 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1060374 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s 1060390 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_10791935800163803658.key 1060405 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns