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.332s | 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.258s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.268s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.218s | 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.392s | 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.284s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.360s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.251s | 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.274s | 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.256s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.399s | 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.269s | 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.302s | 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.354s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.258s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.175s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.263s | 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.655s | 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.302s | 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.368s | 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.206s | 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.259s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.297s | 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.359s | 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.271s | passed |
Standard output
779333 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 779333 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 779333 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.7ns 779337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 782581 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 782597 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 782612 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.19ms 782722 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_2894856298207818815.key 782722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_2894856298207818815.key 782722 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.4ns 782722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 785926 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 785942 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_2894856298207818815.key 785942 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 786377 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 786377 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 786377 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.6ns 786377 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 789522 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 789538 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 789569 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31ms 789679 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_11882016197323231634.key 789679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_11882016197323231634.key 789679 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.2ns 789679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 792920 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 792936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_11882016197323231634.key 792936 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 793048 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10261756803385508033.key 793048 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10261756803385508033.key 793048 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.9ns 793048 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 796114 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 796129 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_10261756803385508033.key 796129 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 796254 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_13928786164252934572.key 796254 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_13928786164252934572.key 796254 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.4ns 796254 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 799388 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 799404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_13928786164252934572.key 799404 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 799514 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17058697845954722574.key 799514 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17058697845954722574.key 799514 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.7ns 799514 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 802679 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 802694 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_17058697845954722574.key 802694 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 802811 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_5909403515035931141.key 802811 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_5909403515035931141.key 802811 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 392.2ns 802811 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 806030 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 806046 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_5909403515035931141.key 806046 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 806171 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_15892095146610237758.key 806171 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_15892095146610237758.key 806171 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.2ns 806171 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 809317 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 809332 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_15892095146610237758.key 809332 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 809442 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6032484114681754609.key 809442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6032484114681754609.key 809442 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 462.4ns 809442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 812646 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 812661 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_6032484114681754609.key 812661 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 812775 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 812775 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 812775 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106ns 812775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 815904 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 815919 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 815919 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 816033 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_17087942881401833167.key 816033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_17087942881401833167.key 816033 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.2ns 816033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 819176 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 819192 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_17087942881401833167.key 819192 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 819301 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13955662469297368673.key 819301 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13955662469297368673.key 819301 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.1ns 819301 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 822387 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 822403 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_13955662469297368673.key 822403 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 822519 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17447355006184512404.key 822519 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17447355006184512404.key 822519 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.4ns 822519 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 825739 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 825802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_17447355006184512404.key 825802 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 825911 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_18097448366664808812.key 825911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_18097448366664808812.key 825911 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 332ns 825911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 829055 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 829087 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_18097448366664808812.key 829087 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 829196 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16243868031022911387.key 829196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16243868031022911387.key 829196 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.6ns 829196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 832416 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 832447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_16243868031022911387.key 832447 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 832557 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_4216342629324106881.key 832557 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_4216342629324106881.key 832557 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 553.1ns 832557 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 835678 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 835693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_4216342629324106881.key 835693 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 835808 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_6083189597814587959.key 835808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_6083189597814587959.key 835808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 476.7ns 835808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 838952 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 838967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_6083189597814587959.key 838967 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 839082 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_16386880280929465528.key 839082 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_16386880280929465528.key 839082 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.3ns 839082 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 842200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 842215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_16386880280929465528.key 842231 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 842340 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14519459206943607665.key 842340 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14519459206943607665.key 842340 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.7ns 842340 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 845483 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 845498 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_14519459206943607665.key 845498 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 845610 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_12000784295532169624.key 845610 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_12000784295532169624.key 845641 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 31.81ms 845641 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 848773 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 848804 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_12000784295532169624.key 848804 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 848913 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_4099818746815567950.key 848913 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_4099818746815567950.key 848913 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.4ns 848913 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 852143 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 852159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_4099818746815567950.key 852159 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 852268 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_9114245797764740948.key 852268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_9114245797764740948.key 852268 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.8ns 852268 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 855385 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 855401 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_9114245797764740948.key 855401 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 855526 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_17854043994627099312.key 855526 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_17854043994627099312.key 855526 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.1ns 855526 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 858576 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 858592 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_17854043994627099312.key 858592 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 858701 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_11391679249297944270.key 858701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_11391679249297944270.key 858701 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.7ns 858701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 861836 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 861852 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_11391679249297944270.key 861852 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns