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.385s | 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.151s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.115s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.217s | 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.171s | 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.041s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.511s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.210s | 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.073s | 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.182s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.353s | 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.268s | 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.130s | 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.379s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.159s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.254s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.115s | 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.180s | 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.144s | 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] | 7.225s | 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.260s | 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.013s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.087s | 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.248s | 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.311s | passed |
Standard output
1174057 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 1174057 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 1174057 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.9ns 1174073 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1179263 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 1179279 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1179294 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.16ms 1179405 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_5615609621997245029.key 1179405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_5615609621997245029.key 1179405 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.6ns 1179405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1184456 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.05s 1184470 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_5615609621997245029.key 1184470 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 1184585 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 1184585 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 1184585 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.4ns 1184585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1189573 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1189589 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1189604 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.17ms 1189729 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15737403710224461609.key 1189729 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15737403710224461609.key 1189729 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.4ns 1189729 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1196822 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 7.09s 1196837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_15737403710224461609.key 1196837 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 1196954 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17894904840891275711.key 1196954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17894904840891275711.key 1196954 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.6ns 1196954 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1202084 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s 1202099 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_17894904840891275711.key 1202099 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1202216 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_1035218724420603047.key 1202216 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_1035218724420603047.key 1202216 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.8ns 1202216 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1207088 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.88s 1207119 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_1035218724420603047.key 1207119 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1207229 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10315097300082300198.key 1207229 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10315097300082300198.key 1207229 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.7ns 1207229 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1212188 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 1212204 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_10315097300082300198.key 1212204 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 492.9ns 1212316 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13894070905317860757.key 1212316 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13894070905317860757.key 1212316 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.8ns 1212316 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1217411 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 1217443 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_13894070905317860757.key 1217443 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1217564 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_16764635651284816041.key 1217564 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_16764635651284816041.key 1217564 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.5ns 1217564 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1222749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s 1222765 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_16764635651284816041.key 1222765 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 1222876 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_3793611327380785748.key 1222876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_3793611327380785748.key 1222876 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 153ns 1222876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1228135 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.25s 1228151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_3793611327380785748.key 1228151 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1228261 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 1228261 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 1228261 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.3ns 1228261 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1233267 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 1233299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1233299 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 1233412 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14407687150755885321.key 1233412 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14407687150755885321.key 1233412 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.4ns 1233412 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1238402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1238418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_14407687150755885321.key 1238418 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 1238527 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8444423959777225485.key 1238527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8444423959777225485.key 1238527 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.5ns 1238527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1243604 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.08s 1243635 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_8444423959777225485.key 1243635 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1243744 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11878264137998217065.key 1243744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11878264137998217065.key 1243744 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.1ns 1243744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1248779 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 1248810 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_11878264137998217065.key 1248810 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1248915 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_14739367869946145570.key 1248915 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_14739367869946145570.key 1248915 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.5ns 1248915 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1253825 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s 1253841 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_14739367869946145570.key 1253841 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1253957 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_1047144209233154044.key 1253957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_1047144209233154044.key 1253957 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.3ns 1253957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1259329 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.37s 1259344 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_1047144209233154044.key 1259360 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1259469 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9263313260409774521.key 1259469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9263313260409774521.key 1259469 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.7ns 1259469 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1264548 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.08s 1264563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_9263313260409774521.key 1264563 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1264679 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_5073987949705313151.key 1264679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_5073987949705313151.key 1264679 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.2ns 1264679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1269610 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.93s 1269626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_5073987949705313151.key 1269626 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 1269752 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6879481038908738772.key 1269752 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6879481038908738772.key 1269752 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.8ns 1269752 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1274789 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.04s 1274821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_6879481038908738772.key 1274821 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1274934 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_16595722358623569317.key 1274934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_16595722358623569317.key 1274934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.6ns 1274934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1280031 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 1280063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_16595722358623569317.key 1280063 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 1280202 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_782280932159252782.key 1280217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_782280932159252782.key 1280217 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.7ns 1280217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1285205 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1285220 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_782280932159252782.key 1285220 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1285333 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_12163610356497970306.key 1285333 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_12163610356497970306.key 1285333 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 826ns 1285333 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1290571 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.24s 1290602 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_12163610356497970306.key 1290602 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1290712 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6110864204657549500.key 1290712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6110864204657549500.key 1290712 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.9ns 1290712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1295742 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 1295757 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_6110864204657549500.key 1295757 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1295871 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_12227049603770107282.key 1295871 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_12227049603770107282.key 1295871 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.4ns 1295871 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1300998 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s 1301014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_12227049603770107282.key 1301014 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1301129 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6348339171935561723.key 1301129 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6348339171935561723.key 1301129 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.9ns 1301129 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1306117 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1306132 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_6348339171935561723.key 1306132 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns