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.399s | 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.450s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.216s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.431s | 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.330s | 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.378s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.344s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.500s | 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.336s | 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.315s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.234s | 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.257s | 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.341s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.338s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.260s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.399s | 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.427s | 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.337s | 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.425s | 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.278s | 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.456s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.270s | 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.642s | 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.229s | passed |
Standard output
785401 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 785401 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 785401 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.6ns 785401 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 788497 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 788512 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 788528 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.74ms 788637 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_14759656830089648328.key 788637 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_14759656830089648328.key 788637 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.8ns 788637 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 791859 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 791953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_14759656830089648328.key 791953 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 792064 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 792064 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 792064 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.9ns 792064 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 795240 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 795256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 795287 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.39ms 795401 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_12453072444712625711.key 795401 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_12453072444712625711.key 795401 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.4ns 795401 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 798685 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 798718 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_12453072444712625711.key 798722 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 798826 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17219058261743193615.key 798826 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17219058261743193615.key 798826 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.7ns 798826 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 801963 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 801994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_17219058261743193615.key 801994 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 802104 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12593263077443230947.key 802104 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_12593263077443230947.key 802104 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.6ns 802104 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 805435 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 805449 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_12593263077443230947.key 805449 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 805560 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_12986497982937172100.key 805560 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_12986497982937172100.key 805560 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.1ns 805560 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 808702 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 808718 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_12986497982937172100.key 808718 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 808830 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_5388414456899170595.key 808830 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_5388414456899170595.key 808830 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.7ns 808830 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 812003 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 812019 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_5388414456899170595.key 812019 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 812472 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_13434782779289200311.key 812472 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_13434782779289200311.key 812472 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.4ns 812472 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 815575 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 815591 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_13434782779289200311.key 815591 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 815701 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_18442579088754475678.key 815701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_18442579088754475678.key 815701 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.5ns 815701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 818973 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 818989 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_18442579088754475678.key 818989 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 819100 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 819100 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 819100 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.3ns 819100 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 822221 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 822236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 822440 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 192.9ms 822550 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14846441549130497900.key 822550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14846441549130497900.key 822550 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.8ns 822550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 825626 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 825657 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_14846441549130497900.key 825657 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 825767 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_17166992285372606663.key 825767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_17166992285372606663.key 825767 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 441.1ns 825767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 829065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 829081 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_17166992285372606663.key 829081 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 829198 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9300066233225611896.key 829198 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9300066233225611896.key 829198 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.5ns 829198 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 832402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 832418 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_9300066233225611896.key 832418 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 832528 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_14526172581825275461.key 832528 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_14526172581825275461.key 832528 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.5ns 832528 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 835764 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 835795 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_14526172581825275461.key 835795 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 835906 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13009231561921682917.key 835906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13009231561921682917.key 835906 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.2ns 835906 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 839095 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 839110 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_13009231561921682917.key 839142 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 839251 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_7724849422666287443.key 839251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_7724849422666287443.key 839251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.4ns 839251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 842618 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 842634 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_7724849422666287443.key 842634 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 842751 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_13038892038398742499.key 842751 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_13038892038398742499.key 842751 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 154ns 842751 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 845962 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 845977 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_13038892038398742499.key 845977 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.6ns 846087 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2600491462031331429.key 846087 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2600491462031331429.key 846087 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.9ns 846087 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 849267 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 849282 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_2600491462031331429.key 849298 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 849405 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_3646996800964052905.key 849405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_3646996800964052905.key 849405 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.3ns 849405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 852529 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 852545 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_3646996800964052905.key 852560 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 852671 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_4776493762952961598.key 852671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_4776493762952961598.key 852671 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.8ns 852671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 855787 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 855802 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_4776493762952961598.key 855802 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 855928 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_5713881029811666639.key 855928 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_5713881029811666639.key 855928 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 441.8ns 855928 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 859138 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 859154 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_5713881029811666639.key 859154 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 859269 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12318441706679630197.key 859269 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12318441706679630197.key 859269 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.2ns 859269 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 862473 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 862488 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_12318441706679630197.key 862488 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 862623 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_15210212722906464216.key 862623 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_15210212722906464216.key 862623 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135ns 862623 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 865739 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 865755 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_15210212722906464216.key 865755 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 865872 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6627742275595289562.key 865872 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6627742275595289562.key 865872 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.3ns 865872 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 869146 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 869162 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_6627742275595289562.key 869162 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns