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] | 5.129s | 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] | 5.096s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.128s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.082s | 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] | 5.081s | 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] | 5.081s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.128s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.097s | 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] | 5.050s | 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] | 5.128s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.164s | 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] | 5.002s | 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] | 5.082s | 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] | 5.048s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.128s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.097s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.080s | 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] | 5.269s | 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] | 5.299s | 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] | 5.113s | 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] | 5.099s | 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] | 5.207s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.143s | 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] | 5.222s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 5.206s | passed |
Standard output
1187843 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 1187858 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 1187858 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns 1187858 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1192877 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s 1192893 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1192908 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.73ms 1193065 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13216964946025685651.key 1193065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13216964946025685651.key 1193065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.4ns 1193065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1198161 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.09s 1198178 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_13216964946025685651.key 1198178 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1198287 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 1198287 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 1198287 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.6ns 1198287 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1203320 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 1203383 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1203477 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 95.09ms 1203586 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_4303549603877997831.key 1203586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_4303549603877997831.key 1203586 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.3ns 1203586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1208574 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1208590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_4303549603877997831.key 1208590 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1208699 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_579768737254002045.key 1208699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_579768737254002045.key 1208699 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.7ns 1208699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1213658 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 1213689 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_579768737254002045.key 1213689 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.4ns 1213798 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_2443436139806144063.key 1213798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_2443436139806144063.key 1213798 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 559.8ns 1213798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1218880 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.07s 1218896 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_2443436139806144063.key 1218896 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1219006 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6527680492915485485.key 1219006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6527680492915485485.key 1219006 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 474.4ns 1219006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1224024 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1224040 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_6527680492915485485.key 1224040 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.4ns 1224149 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_1338501570648512361.key 1224149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_1338501570648512361.key 1224149 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.2ns 1224149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1229230 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.08s 1229262 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_1338501570648512361.key 1229262 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1229371 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_3253383305364586135.key 1229371 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_3253383305364586135.key 1229371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.4ns 1229371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1234436 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.07s 1234468 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_3253383305364586135.key 1234468 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1234577 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_11600408431746742587.key 1234577 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_11600408431746742587.key 1234577 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.8ns 1234577 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1239565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.99s 1239596 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_11600408431746742587.key 1239596 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1239706 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 1239706 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 1239706 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.3ns 1239706 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1244677 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 1244693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1244693 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 1244802 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5604694549398436902.key 1244802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5604694549398436902.key 1244802 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.7ns 1244802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1249790 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.99s 1249821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_5604694549398436902.key 1249821 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1249930 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_14250988763638469449.key 1249930 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_14250988763638469449.key 1249930 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.9ns 1249930 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1254871 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s 1254902 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_14250988763638469449.key 1254902 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1255012 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_12794143593457463313.key 1255012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_12794143593457463313.key 1255012 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.5ns 1255012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1259952 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s 1259983 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_12794143593457463313.key 1259983 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1260093 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_4671640893271245701.key 1260093 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_4671640893271245701.key 1260093 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.2ns 1260093 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1265034 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s 1265049 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_4671640893271245701.key 1265065 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1265174 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16141825789872253273.key 1265174 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16141825789872253273.key 1265174 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 453.8ns 1265174 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1270162 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1270177 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_16141825789872253273.key 1270193 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1270303 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2289438164323293227.key 1270303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2289438164323293227.key 1270303 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.4ns 1270303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1275275 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 1275291 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_2289438164323293227.key 1275291 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1275400 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3308318535397272778.key 1275400 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3308318535397272778.key 1275400 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.8ns 1275400 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1280309 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 1280325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_3308318535397272778.key 1280341 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.8ns 1280450 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_9063762721365393054.key 1280450 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_9063762721365393054.key 1280450 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.6ns 1280450 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1285453 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 1285469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_9063762721365393054.key 1285469 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ns 1285578 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_2121285253294594780.key 1285578 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_2121285253294594780.key 1285578 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.3ns 1285578 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1290441 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.87s 1290472 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_2121285253294594780.key 1290472 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1290581 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_8433596970592998097.key 1290581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_8433596970592998097.key 1290581 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.2ns 1290581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1295523 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 1295554 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_8433596970592998097.key 1295554 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1295664 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_11493539509195458600.key 1295664 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_11493539509195458600.key 1295664 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.8ns 1295664 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1300573 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 1300604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_11493539509195458600.key 1300604 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1300713 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_5969699488256901306.key 1300713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_5969699488256901306.key 1300713 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.8ns 1300713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1305716 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 1305732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_5969699488256901306.key 1305732 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1305841 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_10649488902410875471.key 1305841 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_10649488902410875471.key 1305841 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.7ns 1305841 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1310798 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 1310813 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_10649488902410875471.key 1310829 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 1310938 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6845374608566847664.key 1310938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6845374608566847664.key 1310938 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.9ns 1310938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1315893 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 1315909 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_6845374608566847664.key 1315909 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns