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] | 2.887s | 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] | 2.984s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.887s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.780s | 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] | 2.916s | 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] | 2.899s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.959s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.041s | 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] | 2.925s | 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] | 2.840s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.848s | 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] | 2.798s | 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] | 2.849s | 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] | 2.861s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.923s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.864s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.834s | 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] | 2.909s | 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] | 2.948s | 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] | 2.863s | 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] | 2.788s | 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] | 2.952s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.830s | 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] | 2.802s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 2.812s | passed |
Standard output
683037 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 683037 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 683037 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.4ns 683037 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 685767 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 685782 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 685782 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 685892 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_18011124281845178557.key 685892 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_18011124281845178557.key 685892 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.8ns 685892 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 688664 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 688679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_18011124281845178557.key 688679 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 688792 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 688792 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 688792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.8ns 688792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 691544 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 691559 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 691622 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.44ms 691741 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_11581428690069529601.key 691741 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_11581428690069529601.key 691741 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.2ns 691741 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 694476 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 694492 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_11581428690069529601.key 694492 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 694605 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10144453343475484685.key 694605 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10144453343475484685.key 694605 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.7ns 694605 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 697253 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 697284 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_10144453343475484685.key 697284 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.8ns 697394 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_13632963622419116862.key 697394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_13632963622419116862.key 697394 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.6ns 697394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 700216 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 700231 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_13632963622419116862.key 700231 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 700346 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2419112958042457881.key 700346 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2419112958042457881.key 700346 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 324ns 700346 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 703047 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 703063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_2419112958042457881.key 703063 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 703177 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_5411888062227582818.key 703177 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_5411888062227582818.key 703177 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.3ns 703177 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 705851 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 705866 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_5411888062227582818.key 705866 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 705979 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_9436845018294509931.key 705979 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_9436845018294509931.key 705979 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.9ns 705979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 708661 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 708676 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_9436845018294509931.key 708676 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 708792 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_18127056973184190985.key 708792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_18127056973184190985.key 708792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.75ms 708808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 711548 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 711563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_18127056973184190985.key 711563 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 711679 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 711679 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 711679 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.26ms 711679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 714534 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 714549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 714549 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 714664 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5711181529034795718.key 714664 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5711181529034795718.key 714664 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 218ns 714664 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 717424 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 717440 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_5711181529034795718.key 717440 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 717551 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_4170206806836784753.key 717551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_4170206806836784753.key 717551 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.2ns 717551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 720200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 720215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_4170206806836784753.key 720215 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 720331 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_353363494057526296.key 720331 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_353363494057526296.key 720331 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233ns 720331 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 723122 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 723138 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_353363494057526296.key 723138 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 723247 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9538885849951142779.key 723247 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9538885849951142779.key 723247 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.9ns 723247 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 726006 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 726021 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_9538885849951142779.key 726021 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ns 726147 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_8734766801359558353.key 726147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_8734766801359558353.key 726147 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.2ns 726147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 728945 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 728961 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_8734766801359558353.key 728992 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.1ns 729106 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_16241492356661280362.key 729106 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_16241492356661280362.key 729106 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.9ns 729106 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 732015 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 732031 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_16241492356661280362.key 732031 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.7ns 732147 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_1811800070326886490.key 732147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_1811800070326886490.key 732147 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.7ns 732147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 734945 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 734960 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_1811800070326886490.key 734960 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.4ns 735072 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4452462870433717794.key 735072 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4452462870433717794.key 735072 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.3ns 735072 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 737773 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 737788 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_4452462870433717794.key 737804 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 737913 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_15283961632316425423.key 737913 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_15283961632316425423.key 737913 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.8ns 737913 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 740571 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 740602 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_15283961632316425423.key 740602 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 740712 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7292431414899463246.key 740712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7292431414899463246.key 740712 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.6ns 740712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 743435 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 743451 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_7292431414899463246.key 743451 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 743561 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_15435825385769112451.key 743561 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_15435825385769112451.key 743561 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 352ns 743561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 746282 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 746297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_15435825385769112451.key 746313 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 746422 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_1798000102303674795.key 746422 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_1798000102303674795.key 746422 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.4ns 746422 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 749205 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 749221 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_1798000102303674795.key 749221 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 749346 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_15739416744995675181.key 749346 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_15739416744995675181.key 749346 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.9ns 749346 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 752085 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 752101 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_15739416744995675181.key 752101 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 752210 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3378257124725088533.key 752210 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3378257124725088533.key 752210 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.8ns 752210 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 754914 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 754930 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_3378257124725088533.key 754930 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ns