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.002s | 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.031s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.816s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.706s | 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.819s | 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.889s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.096s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.873s | 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.825s | 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.824s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.016s | 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.857s | 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.914s | 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.993s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.900s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.855s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.864s | 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.898s | 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.050s | 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.876s | 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.917s | 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.933s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.753s | 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.020s | 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.785s | passed |
Standard output
1121490 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 1121490 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 1121490 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.5ns 1121490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1126355 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s 1126370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1126370 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ms 1126496 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_343192718777025716.key 1126496 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_343192718777025716.key 1126496 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.7ns 1126496 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1131247 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.75s 1131278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_343192718777025716.key 1131278 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1131394 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 1131394 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 1131394 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.8ns 1131394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1136288 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 1136303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1136319 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.23ms 1136444 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_16671954733592368397.key 1136444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_16671954733592368397.key 1136444 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.1ns 1136444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1141179 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.74s 1141195 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_16671954733592368397.key 1141210 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1141320 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_1935235393106424240.key 1141320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_1935235393106424240.key 1141320 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.6ns 1141320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1146108 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.78s 1146123 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_1935235393106424240.key 1146123 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1146239 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12367541352873667542.key 1146239 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12367541352873667542.key 1146239 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.8ns 1146239 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1151044 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.8s 1151060 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_12367541352873667542.key 1151060 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1151172 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17495323949864215141.key 1151172 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17495323949864215141.key 1151172 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.4ns 1151172 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1155799 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.62s 1155815 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_17495323949864215141.key 1155815 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 488.6ns 1155925 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_16128057717499854593.key 1155925 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_16128057717499854593.key 1155925 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.9ns 1155925 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1160645 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.72s 1160837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_16128057717499854593.key 1160837 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 1160946 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_3071353086212191146.key 1160946 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_3071353086212191146.key 1160946 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.3ns 1160946 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1165590 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.65s 1165605 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_3071353086212191146.key 1165621 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ns 1165731 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_1823932430797076878.key 1165731 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_1823932430797076878.key 1165731 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.8ns 1165731 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1170593 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s 1170609 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_1823932430797076878.key 1170609 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1170734 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 1170734 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 1170734 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.9ns 1170734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1175625 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 1175640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1175656 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 1175766 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_12279281859633430203.key 1175766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_12279281859633430203.key 1175766 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.5ns 1175766 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1180441 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 1180456 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_12279281859633430203.key 1180456 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 1180583 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_16513128632115626235.key 1180583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_16513128632115626235.key 1180583 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.6ns 1180583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1185162 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.58s 1185178 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_16513128632115626235.key 1185178 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1185289 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10252666547469057553.key 1185289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10252666547469057553.key 1185289 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.4ns 1185289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1189967 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.69s 1189999 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_10252666547469057553.key 1189999 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1190108 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_8385654420795524538.key 1190108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_8385654420795524538.key 1190108 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.5ns 1190108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1194860 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.76s 1194892 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_8385654420795524538.key 1194892 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1194997 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14019107204385768785.key 1194997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14019107204385768785.key 1194997 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.84ms 1194997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1199953 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 1199969 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_14019107204385768785.key 1199985 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1200098 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_1066132635938637078.key 1200098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_1066132635938637078.key 1200098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.4ns 1200098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1204836 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.74s 1204851 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_1066132635938637078.key 1204851 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.7ns 1204967 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_9491955393423408361.key 1204967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_9491955393423408361.key 1204967 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.9ns 1204967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1209663 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.7s 1209678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_9491955393423408361.key 1209678 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1209792 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6475435355003576569.key 1209792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6475435355003576569.key 1209792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.1ns 1209792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1214484 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.69s 1214500 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_6475435355003576569.key 1214500 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 1214616 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_9921298783033045215.key 1214616 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_9921298783033045215.key 1214616 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.4ns 1214616 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1219333 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.72s 1219348 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_9921298783033045215.key 1219364 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1219473 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11752924201887424235.key 1219473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11752924201887424235.key 1219473 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.8ns 1219473 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1224243 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.77s 1224274 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_11752924201887424235.key 1224274 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1224388 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_11279179795575250205.key 1224388 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_11279179795575250205.key 1224388 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.1ns 1224388 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1229252 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s 1229268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_11279179795575250205.key 1229268 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1229381 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3168704363634164917.key 1229381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3168704363634164917.key 1229381 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.4ns 1229381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1234159 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.77s 1234170 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_3168704363634164917.key 1234170 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1234281 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_231053909977835243.key 1234281 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_231053909977835243.key 1234281 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 149ns 1234281 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1239009 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.73s 1239025 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_231053909977835243.key 1239025 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1239140 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6195027387981226324.key 1239140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6195027387981226324.key 1239140 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.6ns 1239140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1243877 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.73s 1243892 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_6195027387981226324.key 1243892 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns