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.800s | 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.808s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.803s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.809s | 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.777s | 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.822s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.800s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.830s | 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.781s | 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.830s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.919s | 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.812s | 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.817s | 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.788s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.812s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.794s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.806s | 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.826s | 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.897s | 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.862s | 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.816s | 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.842s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.832s | 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.763s | 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
652016 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 652016 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 652016 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 652016 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 654794 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 654809 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 654825 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 654934 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_440965917862407137.key 654934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_440965917862407137.key 654934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.3ns 654934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 657628 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 657644 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_440965917862407137.key 657644 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 657758 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 657758 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 657758 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.7ns 657758 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 660505 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 660521 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 660536 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.83ms 660656 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_8705798502813197189.key 660656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_8705798502813197189.key 660656 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225ns 660656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 663393 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 663409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_8705798502813197189.key 663409 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 663518 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_9816368406313103538.key 663518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_9816368406313103538.key 663518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.1ns 663518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 666194 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 666209 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_9816368406313103538.key 666225 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 666334 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_1579160666435898111.key 666334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_1579160666435898111.key 666334 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.6ns 666334 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 669050 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 669065 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_1579160666435898111.key 669065 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 669176 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_15455391588800997634.key 669176 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_15455391588800997634.key 669176 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.3ns 669176 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 671881 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 671897 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_15455391588800997634.key 671897 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 672008 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_17341670355563982773.key 672008 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_17341670355563982773.key 672008 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.2ns 672008 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 674646 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 674662 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_17341670355563982773.key 674662 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 674771 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_7992254937906871811.key 674771 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_7992254937906871811.key 674771 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 222ns 674771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 677460 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 677475 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_7992254937906871811.key 677475 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 677585 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13961620340713617896.key 677585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13961620340713617896.key 677585 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.2ns 677585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 680254 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 680269 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_13961620340713617896.key 680269 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 680384 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 680384 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 680384 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.7ns 680384 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 683067 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 683082 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 683082 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 683192 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_2854826259606088716.key 683192 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_2854826259606088716.key 683192 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 358.5ns 683192 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 685869 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 685884 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_2854826259606088716.key 685884 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 685997 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5004865352886125888.key 685997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5004865352886125888.key 685997 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.5ns 685997 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 688678 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 688693 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_5004865352886125888.key 688693 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 688807 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_5992055584644301841.key 688807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_5992055584644301841.key 688807 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.6ns 688807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 691452 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 691467 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_5992055584644301841.key 691467 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 691584 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_8637659770807539854.key 691584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_8637659770807539854.key 691584 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.4ns 691584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 694275 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 694291 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_8637659770807539854.key 694291 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 694406 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16307900638213585977.key 694406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16307900638213585977.key 694406 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.6ns 694406 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 697082 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 697098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_16307900638213585977.key 697098 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 697207 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9026327759660339968.key 697207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9026327759660339968.key 697207 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.4ns 697207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 699913 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 699913 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_9026327759660339968.key 699913 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 700038 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_6163082996252283471.key 700038 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_6163082996252283471.key 700038 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.5ns 700038 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 702694 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 702710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_6163082996252283471.key 702710 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 702819 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_429844141938314203.key 702819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_429844141938314203.key 702819 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.1ns 702819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 705524 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 705540 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_429844141938314203.key 705540 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 705650 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13106539034771164301.key 705650 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13106539034771164301.key 705650 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.4ns 705650 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 708328 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 708344 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_13106539034771164301.key 708344 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 708461 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14628572592366855420.key 708461 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14628572592366855420.key 708461 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.9ns 708461 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 711137 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 711152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_14628572592366855420.key 711152 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 711277 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_11968358616261869144.key 711277 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_11968358616261869144.key 711277 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.2ns 711277 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 713942 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 713957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_11968358616261869144.key 713957 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 714067 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_17662393798733657502.key 714067 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_17662393798733657502.key 714067 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.4ns 714067 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 716749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 716765 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_17662393798733657502.key 716765 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 716879 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_16441617205420218386.key 716879 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_16441617205420218386.key 716879 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.9ns 716879 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 719549 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 719565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_16441617205420218386.key 719565 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 719674 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_10460855973001982321.key 719674 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_10460855973001982321.key 719674 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 130ns 719674 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 722356 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 722371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_10460855973001982321.key 722371 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns