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.828s | 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.816s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.916s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.029s | 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.859s | 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.895s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.838s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.907s | 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.759s | 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.884s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.990s | 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.855s | 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.897s | 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.792s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.912s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.806s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.953s | 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.095s | 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.892s | 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.860s | 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.813s | 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.881s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.081s | 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.823s | 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.897s | passed |
Standard output
695737 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 695738 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 695738 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.3ns 695744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 698571 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 698586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 698602 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.19ms 698715 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_6974723984668284554.key 698715 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_6974723984668284554.key 698715 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.7ns 698715 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 701539 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 701695 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_6974723984668284554.key 701697 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ns 701810 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 701810 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 701810 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.2ns 701810 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 704546 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 704562 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 704593 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.44ms 704702 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_10287408127191580062.key 704702 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_10287408127191580062.key 704702 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.4ns 704702 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 707423 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 707454 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_10287408127191580062.key 707454 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ns 707563 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_7075498164258012549.key 707563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_7075498164258012549.key 707563 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.6ns 707563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 710237 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 710254 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_7075498164258012549.key 710254 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ns 710378 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_13101459018854205628.key 710378 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_13101459018854205628.key 710378 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.4ns 710378 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 713114 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 713146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_13101459018854205628.key 713146 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ns 713259 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_4222865322523944531.key 713259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_4222865322523944531.key 713259 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.2ns 713259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 716168 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 716230 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_4222865322523944531.key 716230 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ns 716341 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13117581784197861530.key 716341 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13117581784197861530.key 716341 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.7ns 716341 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 719034 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 719050 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_13117581784197861530.key 719050 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 719166 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_8872611859903673958.key 719166 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_8872611859903673958.key 719166 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.1ns 719166 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 721933 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 721949 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_8872611859903673958.key 721949 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ns 722064 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4121503347412426955.key 722064 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4121503347412426955.key 722064 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 531.3ns 722064 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 724760 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 724775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_4121503347412426955.key 724775 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ns 724892 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 724892 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 724892 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.1ns 724892 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 727567 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 727598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 727598 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 727709 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_13894488556993496306.key 727709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_13894488556993496306.key 727709 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.5ns 727709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 730455 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 730486 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_13894488556993496306.key 730518 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.6ns 730627 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5299053135367941117.key 730627 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5299053135367941117.key 730627 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 402ns 730627 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 733528 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 733543 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_5299053135367941117.key 733543 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 733657 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_2178822855839726339.key 733657 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_2178822855839726339.key 733657 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.7ns 733657 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 736388 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 736404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_2178822855839726339.key 736404 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.6ns 736518 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_10893541672164020964.key 736518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_10893541672164020964.key 736518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.5ns 736518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 739272 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 739303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_10893541672164020964.key 739303 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 739413 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13845408552641306222.key 739413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13845408552641306222.key 739413 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.1ns 739413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 742127 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 742143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_13845408552641306222.key 742143 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ns 742252 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_1565424244335770915.key 742252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_1565424244335770915.key 742252 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259ns 742252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 745019 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 745035 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_1565424244335770915.key 745052 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.1ns 745160 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3094639189224868258.key 745160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3094639189224868258.key 745160 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.2ns 745160 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 747789 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 747805 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_3094639189224868258.key 747805 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 747920 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_13178668474688727835.key 747920 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_13178668474688727835.key 747920 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.9ns 747920 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 750672 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 750687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_13178668474688727835.key 750687 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ns 750804 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_16943299549541397542.key 750804 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_16943299549541397542.key 750804 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.9ns 750804 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 753520 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 753552 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_16943299549541397542.key 753552 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ns 753661 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11319076220001603961.key 753661 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_11319076220001603961.key 753661 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.5ns 753661 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 756428 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 756444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_11319076220001603961.key 756444 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ns 756558 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_8746553091355914456.key 756558 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_8746553091355914456.key 756558 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.6ns 756558 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 759210 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 759226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_8746553091355914456.key 759226 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 759351 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_10385511363463595758.key 759351 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_10385511363463595758.key 759351 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.4ns 759351 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 762123 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 762154 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_10385511363463595758.key 762154 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ns 762263 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_13704696427205869186.key 762263 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_13704696427205869186.key 762263 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.3ns 762263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 764931 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 764947 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_13704696427205869186.key 764962 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ns 765072 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_334732391778139279.key 765072 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_334732391778139279.key 765072 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.4ns 765072 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 767886 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 767901 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_334732391778139279.key 767901 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ns