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.246s | 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.232s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.231s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.191s | 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.209s | 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.292s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.268s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.216s | 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.192s | 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.236s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.274s | 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.213s | 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.328s | 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.209s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.263s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.179s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.247s | 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.268s | 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.461s | 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.214s | 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.210s | 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.331s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.304s | 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.208s | 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.313s | passed |
Standard output
792246 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 792246 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 792246 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.4ns 792246 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 795383 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 795398 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 795414 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.96ms 795523 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17102911893588002304.key 795523 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17102911893588002304.key 795523 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.6ns 795523 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 798666 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 798681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_17102911893588002304.key 798681 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 798791 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 798791 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 798791 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.8ns 798791 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 802090 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 802105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 802137 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.34ms 802252 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_10063380791170032766.key 802252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_10063380791170032766.key 802252 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 217ns 802252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 805340 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 805355 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_10063380791170032766.key 805355 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 805466 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_11786932005432909635.key 805466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_11786932005432909635.key 805466 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.2ns 805466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 808544 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 808560 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_11786932005432909635.key 808560 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ns 808676 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_3814145593947897660.key 808676 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_3814145593947897660.key 808676 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.4ns 808676 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 811756 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 811787 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_3814145593947897660.key 811787 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 812009 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_9439117697325659106.key 812010 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_9439117697325659106.key 812011 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 488.4ns 812013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 815169 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 815185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_9439117697325659106.key 815200 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 815311 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_1144951492599012561.key 815311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_1144951492599012561.key 815311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142ns 815311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 818391 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 818407 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_1144951492599012561.key 818407 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 818519 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_16453399456902846327.key 818519 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_16453399456902846327.key 818519 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.4ns 818519 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 821702 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 821718 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_16453399456902846327.key 821718 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 821832 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5551537466027011276.key 821832 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5551537466027011276.key 821832 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.6ns 821832 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 824938 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 824969 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5551537466027011276.key 824969 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 825078 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 825078 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 825078 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.1ns 825078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 828182 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 828198 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 828198 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 828310 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_4346800251205595195.key 828310 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_4346800251205595195.key 828310 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.7ns 828310 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 831368 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 831399 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_4346800251205595195.key 831430 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 831542 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_9524733967743338816.key 831542 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_9524733967743338816.key 831542 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.2ns 831542 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 834593 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 834609 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_9524733967743338816.key 834624 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ns 834734 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_6402601792054139625.key 834734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_6402601792054139625.key 834734 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.4ns 834734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 837815 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 837830 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_6402601792054139625.key 837830 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 837944 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_3251643009529382415.key 837944 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_3251643009529382415.key 837944 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.9ns 837944 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 841110 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 841126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_3251643009529382415.key 841126 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ns 841236 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_8264801682445359508.key 841236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_8264801682445359508.key 841236 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.8ns 841236 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 844363 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 844389 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_8264801682445359508.key 844395 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 844505 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_4685605790820548727.key 844505 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_4685605790820548727.key 844505 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.3ns 844505 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 847591 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 847607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_4685605790820548727.key 847607 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 847721 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3633584581090341345.key 847721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_3633584581090341345.key 847721 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.1ns 847721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 850788 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 850803 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_3633584581090341345.key 850803 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ns 850913 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_14591326173985264676.key 850913 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_14591326173985264676.key 850913 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.5ns 850913 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 854024 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 854039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_14591326173985264676.key 854039 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 854149 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_12981751667742808197.key 854149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_12981751667742808197.key 854149 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.8ns 854149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 857232 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 857248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_12981751667742808197.key 857248 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 857362 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_17914719310024921688.key 857362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_17914719310024921688.key 857362 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.3ns 857362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 860565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 860581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_17914719310024921688.key 860581 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ns 860690 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_13377653607228998462.key 860690 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_13377653607228998462.key 860690 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 546.1ns 860690 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 863772 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 863787 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_13377653607228998462.key 863787 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 863900 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_11466254262675505919.key 863900 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_11466254262675505919.key 863900 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.4ns 863900 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 867038 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 867053 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_11466254262675505919.key 867053 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ns 867163 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_11489358831740875872.key 867163 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_11489358831740875872.key 867163 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 141ns 867163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 870215 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 870231 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_11489358831740875872.key 870231 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 870344 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3704333017954518357.key 870344 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3704333017954518357.key 870344 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.4ns 870344 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 873450 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 873466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_3704333017954518357.key 873466 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns