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.034s | 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.113s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.190s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.036s | 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.143s | 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.111s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.158s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.035s | 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.142s | 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.098s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.269s | 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.143s | 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.239s | 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.190s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.066s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.190s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.254s | 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.190s | 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.207s | 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.174s | 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.161s | 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.065s | 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.098s | 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.099s | passed |
Standard output
1186799 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 1186799 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 1186799 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.4ns 1186799 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1191929 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s 1191945 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1191960 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.36ms 1192070 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8547017443541494829.key 1192070 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8547017443541494829.key 1192070 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.1ns 1192070 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1197120 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.04s 1197135 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_8547017443541494829.key 1197135 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1197260 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 1197260 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 1197260 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.4ns 1197260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1202311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.04s 1202327 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1202358 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.6ms 1202468 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_6239142277108885781.key 1202468 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_6239142277108885781.key 1202468 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 383ns 1202468 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1207502 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 1207517 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_6239142277108885781.key 1207533 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 1207642 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8477872746341384170.key 1207642 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8477872746341384170.key 1207642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.3ns 1207642 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1212677 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 1212693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_8477872746341384170.key 1212693 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1212803 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7704854280088583894.key 1212803 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7704854280088583894.key 1212803 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.5ns 1212803 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1217743 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.93s 1217758 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_7704854280088583894.key 1217758 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1217868 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_9354191440684214091.key 1217868 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_9354191440684214091.key 1217868 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.5ns 1217868 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1222886 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1222902 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_9354191440684214091.key 1222902 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.7ns 1223011 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_11638099083587353270.key 1223011 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_11638099083587353270.key 1223011 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.8ns 1223011 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1227968 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 1227984 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_11638099083587353270.key 1227999 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1228109 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_11679228470733703243.key 1228109 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_11679228470733703243.key 1228109 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.7ns 1228109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1233083 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 1233098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_11679228470733703243.key 1233098 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1233208 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_9391575891715285491.key 1233208 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_9391575891715285491.key 1233208 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.9ns 1233208 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1238102 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 1238133 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_9391575891715285491.key 1238133 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 1238242 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 1238242 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 1238242 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.6ns 1238242 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1243214 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 1243230 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1243245 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 1243355 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3972227239281785852.key 1243355 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3972227239281785852.key 1243355 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 504ns 1243355 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1248420 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.06s 1248436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_3972227239281785852.key 1248436 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 1248545 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13756746300711811077.key 1248545 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13756746300711811077.key 1248545 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.7ns 1248545 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1253456 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 1253472 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_13756746300711811077.key 1253472 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.1ns 1253581 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_418693004298411803.key 1253581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_418693004298411803.key 1253581 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 384ns 1253581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1258583 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 1258614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_418693004298411803.key 1258614 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1258724 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_7188531860490631524.key 1258724 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_7188531860490631524.key 1258724 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 295ns 1258724 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1263697 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1263728 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_7188531860490631524.key 1263728 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1263838 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_6671329521160760989.key 1263838 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_6671329521160760989.key 1263838 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 453.6ns 1263838 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1268855 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1268871 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_6671329521160760989.key 1268887 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ns 1268997 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9819733054201602070.key 1268997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9819733054201602070.key 1268997 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.9ns 1268997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1273890 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 1273906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_9819733054201602070.key 1273906 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1274032 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_5836955967172045686.key 1274032 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_5836955967172045686.key 1274032 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.3ns 1274032 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1279049 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1279065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_5836955967172045686.key 1279065 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13ns 1279174 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_14749671020544271836.key 1279174 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_14749671020544271836.key 1279174 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 434.3ns 1279174 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1284131 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 1284163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_14749671020544271836.key 1284163 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1284272 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_3851183107319457555.key 1284272 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_3851183107319457555.key 1284272 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.7ns 1284272 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1289275 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 1289306 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_3851183107319457555.key 1289306 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1289415 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_16990637183527788565.key 1289415 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_16990637183527788565.key 1289415 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.2ns 1289415 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1294513 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 1294545 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_16990637183527788565.key 1294545 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 1294654 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_265929309299620923.key 1294654 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_265929309299620923.key 1294654 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 447.8ns 1294654 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1299704 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.05s 1299720 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_265929309299620923.key 1299736 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1299845 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_384559515822640927.key 1299845 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_384559515822640927.key 1299845 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.8ns 1299845 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1304786 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s 1304801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_384559515822640927.key 1304801 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.5ns 1304911 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_1112537988675574601.key 1304911 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_1112537988675574601.key 1304911 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.2ns 1304911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1309960 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.05s 1309991 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_1112537988675574601.key 1309991 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1310101 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_17397985019379004061.key 1310101 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_17397985019379004061.key 1310101 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 446.2ns 1310101 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1315214 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s 1315246 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_17397985019379004061.key 1315246 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns