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] | 3.074s | 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] | 3.018s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.094s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.034s | 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] | 3.045s | 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] | 3.072s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.076s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.050s | 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] | 3.083s | 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] | 3.092s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.176s | 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] | 3.214s | 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] | 3.320s | 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] | 3.269s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.166s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.367s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.216s | 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] | 3.285s | 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] | 3.184s | 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] | 3.176s | 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] | 3.071s | 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] | 3.083s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.054s | 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] | 3.042s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 3.060s | passed |
Standard output
766911 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 766911 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 766911 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 766911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 769937 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 769953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 769968 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.61ms 770078 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1886645802290691914.key 770078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1886645802290691914.key 770078 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.2ns 770078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 773232 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 773232 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_1886645802290691914.key 773232 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 773363 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 773363 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 773363 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.8ns 773363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 776390 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 776406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 776437 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.2ms 776547 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_8512423911932198007.key 776547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_8512423911932198007.key 776547 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.6ns 776547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 779536 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 779598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_8512423911932198007.key 779598 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 779723 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_9457765512521170412.key 779723 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_9457765512521170412.key 779723 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.9ns 779723 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 782663 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 782679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_9457765512521170412.key 782679 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 782794 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7734336317246695787.key 782794 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7734336317246695787.key 782794 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.2ns 782794 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 785752 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 785767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_7734336317246695787.key 785767 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 785877 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_15229343269654952344.key 785877 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_15229343269654952344.key 785877 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.4ns 785877 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 788801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 788817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_15229343269654952344.key 788817 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 788931 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_11874618574471160223.key 788931 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_11874618574471160223.key 788931 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.5ns 788931 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 791848 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 791864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_11874618574471160223.key 791864 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.6ns 791973 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_15906066091324284649.key 791973 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_15906066091324284649.key 791973 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.1ns 791973 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 794908 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 794923 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_15906066091324284649.key 794923 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 795033 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6249773483064665923.key 795033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6249773483064665923.key 795033 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.3ns 795033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 797977 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 797993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_6249773483064665923.key 797993 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 798107 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 798107 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 798107 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.5ns 798107 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 800998 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 801014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 801014 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 801125 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_8165602584311825294.key 801125 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_8165602584311825294.key 801125 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 419ns 801125 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 804094 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 804109 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_8165602584311825294.key 804109 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 804219 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11887250986816813683.key 804219 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11887250986816813683.key 804219 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.8ns 804219 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 807127 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 807143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_11887250986816813683.key 807143 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 807253 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_4386330515106628522.key 807253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_4386330515106628522.key 807253 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.5ns 807253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 810172 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 810188 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_4386330515106628522.key 810188 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 810298 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_136831334783270992.key 810298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_136831334783270992.key 810298 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.1ns 810298 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 813245 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 813260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_136831334783270992.key 813260 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 813370 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4747530647240438947.key 813370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4747530647240438947.key 813370 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.9ns 813370 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 816318 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 816333 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_4747530647240438947.key 816333 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 816446 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_16782922822196625877.key 816446 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_16782922822196625877.key 816446 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.7ns 816446 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 819371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 819371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_16782922822196625877.key 819386 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 819496 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_11174378050857415637.key 819496 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_11174378050857415637.key 819496 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.4ns 819496 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 822454 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 822470 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_11174378050857415637.key 822470 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 822579 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_13759157322058522983.key 822579 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_13759157322058522983.key 822579 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.5ns 822579 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 825542 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 825558 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_13759157322058522983.key 825558 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 825671 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_7659956671097200744.key 825671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_7659956671097200744.key 825671 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 296ns 825671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 828759 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 828775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_7659956671097200744.key 828775 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 828885 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_17690738473054852591.key 828885 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_17690738473054852591.key 828885 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.7ns 828885 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 832076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 832092 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_17690738473054852591.key 832092 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 832205 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_13950429139312019294.key 832205 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_13950429139312019294.key 832205 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.2ns 832205 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 835349 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 835365 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_13950429139312019294.key 835365 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 835474 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_1408661881088016064.key 835474 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_1408661881088016064.key 835474 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.5ns 835474 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 838513 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 838530 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_1408661881088016064.key 838530 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 838640 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_1748623737643027577.key 838640 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_1748623737643027577.key 838640 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.3ns 838640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 841882 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 841898 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_1748623737643027577.key 841898 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 842007 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_1716347846012833430.key 842007 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_1716347846012833430.key 842007 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.3ns 842007 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 845098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 845113 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_1716347846012833430.key 845113 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns