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.295s | 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.040s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.068s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.990s | 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.024s | 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.010s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.480s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.058s | 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.129s | 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.062s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.974s | 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.055s | 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.008s | 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.143s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.131s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.095s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.110s | 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.043s | 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.196s | 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.204s | 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.344s | 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.000s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.073s | 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.033s | 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.132s | passed |
Standard output
729279 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 729282 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 729282 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227ns 729285 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 732102 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 732118 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 732133 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.86ms 732243 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_15280167813838828363.key 732243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_15280167813838828363.key 732243 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.8ns 732243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 735159 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 735175 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_15280167813838828363.key 735175 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 735286 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 735286 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 735286 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.9ns 735286 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 738292 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 738323 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 738371 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.64ms 738482 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_16375471346854142846.key 738482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_16375471346854142846.key 738482 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.3ns 738482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 741545 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 741561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_16375471346854142846.key 741561 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 741686 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12779541135136056805.key 741686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12779541135136056805.key 741686 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 214ns 741686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 744898 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 744914 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_12779541135136056805.key 744914 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 745030 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7296735631790174519.key 745030 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7296735631790174519.key 745030 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.5ns 745030 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 747901 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 747917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_7296735631790174519.key 747917 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 748030 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_18042139402534591879.key 748030 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_18042139402534591879.key 748030 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.3ns 748030 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 750977 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 750993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_18042139402534591879.key 750993 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 751103 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_5277940930986843568.key 751103 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_5277940930986843568.key 751103 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.4ns 751103 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 754011 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 754027 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_5277940930986843568.key 754027 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 754136 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_4446124588260548480.key 754136 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_4446124588260548480.key 754136 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.9ns 754136 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 757143 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 757159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_4446124588260548480.key 757159 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 757268 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_17935380697344184060.key 757268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_17935380697344184060.key 757268 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.3ns 757268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 760415 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 760432 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_17935380697344184060.key 760447 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 760563 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 760563 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 760563 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.6ns 760563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 763475 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 763491 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 763491 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 763603 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5604989288564144924.key 763603 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5604989288564144924.key 763603 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.3ns 763603 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 766547 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 766562 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_5604989288564144924.key 766562 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 766672 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5840078366127115461.key 766672 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5840078366127115461.key 766672 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.3ns 766672 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 769534 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 769550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_5840078366127115461.key 769550 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 769662 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_3801161583373615102.key 769662 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_3801161583373615102.key 769662 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 152ns 769662 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 772545 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 772576 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_3801161583373615102.key 772576 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 772686 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_3515033765908216090.key 772686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_3515033765908216090.key 772686 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.7ns 772686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 775568 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 775583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_3515033765908216090.key 775583 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 775696 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_8801917189380833756.key 775696 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_8801917189380833756.key 775696 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 416.9ns 775696 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 778994 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 779009 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_8801917189380833756.key 779025 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 779193 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_16106747978540200006.key 779193 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_16106747978540200006.key 779193 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 567.4ns 779193 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 782105 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 782121 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_16106747978540200006.key 782121 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 782235 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_708755140059495968.key 782235 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_708755140059495968.key 782235 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.3ns 782235 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 785239 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 785255 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_708755140059495968.key 785255 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 785364 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2434930886902825942.key 785364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2434930886902825942.key 785364 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.9ns 785364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 788298 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 788313 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_2434930886902825942.key 788313 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 788426 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11858606211637025348.key 788426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11858606211637025348.key 788426 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.6ns 788426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 791349 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 791365 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_11858606211637025348.key 791365 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 791481 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1214219219321186948.key 791481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1214219219321186948.key 791481 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.8ns 791481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 794358 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 794380 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_1214219219321186948.key 794380 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 794489 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_16381614966722297831.key 794489 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_16381614966722297831.key 794489 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.3ns 794489 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 797469 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 797485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_16381614966722297831.key 797485 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 797632 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_7091059042928197365.key 797632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_7091059042928197365.key 797632 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 673.2ns 797632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 800639 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 800655 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_7091059042928197365.key 800655 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 800764 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_6392666529618147136.key 800764 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_6392666529618147136.key 800764 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.2ns 800764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 803728 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 803743 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_6392666529618147136.key 803743 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 803860 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3106183151215451528.key 803860 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3106183151215451528.key 803860 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 434.6ns 803860 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 806840 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 806856 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_3106183151215451528.key 806856 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns