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.906s | 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.968s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.824s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.049s | 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.895s | 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.012s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.973s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.136s | 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.946s | 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.047s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.991s | 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.932s | 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.957s | 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.017s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.964s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.959s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.137s | 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.941s | 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.927s | 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.985s | 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.011s | 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.987s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.853s | 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.912s | 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.902s | passed |
Standard output
684758 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 684758 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 684758 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 684758 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 687603 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 687618 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 687618 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.17ms 687734 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17645629511555966412.key 687734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17645629511555966412.key 687734 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 687734 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 690533 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 690548 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_17645629511555966412.key 690548 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 690676 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 690676 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 690676 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 463.2ns 690691 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 693458 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 693458 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 693490 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.52ms 693603 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_17848010890270466007.key 693603 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_17848010890270466007.key 693603 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.3ns 693603 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 696464 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 696480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_17848010890270466007.key 696480 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 696589 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12379863904080097382.key 696589 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12379863904080097382.key 696589 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.2ns 696589 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 699469 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 699485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_12379863904080097382.key 699485 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 699600 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7432505291438811783.key 699600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_7432505291438811783.key 699600 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.7ns 699600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 702462 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 702478 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_7432505291438811783.key 702478 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 702588 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6727567294637282115.key 702588 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6727567294637282115.key 702588 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.1ns 702588 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 705316 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 705332 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_6727567294637282115.key 705332 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 705441 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_2806026515096748845.key 705441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_2806026515096748845.key 705441 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.9ns 705441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 708229 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 708244 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_2806026515096748845.key 708244 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 708354 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_11285159088475759728.key 708354 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_11285159088475759728.key 708354 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.5ns 708354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 711126 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 711142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_11285159088475759728.key 711142 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 711256 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_7901525433378217608.key 711256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_7901525433378217608.key 711256 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.6ns 711256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 714038 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 714054 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_7901525433378217608.key 714054 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 714163 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 714163 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 714163 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 714163 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 716991 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 717007 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 717022 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 717132 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_8711169541844574836.key 717132 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_8711169541844574836.key 717132 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.6ns 717132 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 719832 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 719848 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_8711169541844574836.key 719848 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 719957 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5483222792234062418.key 719957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_5483222792234062418.key 719957 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183ns 719957 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 722871 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 722886 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_5483222792234062418.key 722886 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 723007 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10765420261542418837.key 723007 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_10765420261542418837.key 723007 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.7ns 723007 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 725778 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 725794 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_10765420261542418837.key 725794 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 725904 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_17504188597888669573.key 725904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_17504188597888669573.key 725904 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.5ns 725904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 728785 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 728801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_17504188597888669573.key 728801 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 728915 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14564031321229526884.key 728915 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14564031321229526884.key 728915 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.2ns 728915 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 731761 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 731776 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_14564031321229526884.key 731776 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 731890 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_5588609568961075533.key 731890 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_5588609568961075533.key 731890 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.4ns 731890 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 734897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 734915 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_5588609568961075533.key 734915 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 735026 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_17387814881522193285.key 735026 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_17387814881522193285.key 735026 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 396.6ns 735026 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 737846 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 737862 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_17387814881522193285.key 737862 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 737974 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_10757639237505432522.key 737974 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_10757639237505432522.key 737974 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.4ns 737974 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 740889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 740905 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_10757639237505432522.key 740905 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 741021 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_453481599371292923.key 741021 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_453481599371292923.key 741021 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 864.4ns 741021 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 743823 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 743839 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_453481599371292923.key 743839 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 743953 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9867330390835972299.key 743953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9867330390835972299.key 743953 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 526.2ns 743953 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 746786 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 746801 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_9867330390835972299.key 746801 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 746911 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_12789313947657711770.key 746911 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_12789313947657711770.key 746911 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.8ns 746911 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 749803 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 749819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_12789313947657711770.key 749819 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 749928 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_1843982582195385349.key 749928 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_1843982582195385349.key 749928 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.9ns 749928 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 752761 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 752777 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_1843982582195385349.key 752777 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 752893 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_11397354567387898155.key 752893 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_11397354567387898155.key 752893 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.7ns 752893 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 755722 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 755738 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_11397354567387898155.key 755738 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 755854 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_8313943597246005783.key 755854 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_8313943597246005783.key 755854 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.3ns 755854 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 758857 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 758873 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_8313943597246005783.key 758888 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns