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] | 4.064s | 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] | 4.134s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.064s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.065s | 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] | 4.050s | 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] | 4.049s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.049s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.049s | 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] | 4.096s | 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] | 4.596s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.082s | 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.923s | 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.958s | 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.939s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.893s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.908s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.892s | 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] | 4.017s | 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] | 4.034s | 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] | 4.033s | 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] | 4.033s | 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] | 4.003s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.003s | 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.986s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 4.018s | passed |
Standard output
901523 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 901523 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 901523 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93ns 901523 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 905463 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s 905478 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 905478 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 905604 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_14790510654352622749.key 905604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_14790510654352622749.key 905604 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.4ns 905604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 909480 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 909497 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_14790510654352622749.key 909512 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 909621 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 909621 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 909621 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.3ns 909621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 913514 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 913530 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 913545 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.3ms 913655 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15563598997437455205.key 913655 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15563598997437455205.key 913655 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.7ns 913655 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 917563 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.91s 917579 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_15563598997437455205.key 917579 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 917688 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10200717182123360424.key 917688 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10200717182123360424.key 917688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.3ns 917688 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 921596 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.91s 921612 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_10200717182123360424.key 921612 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 921721 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8743716903167871370.key 921721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_8743716903167871370.key 921721 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.9ns 921721 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 925599 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 925615 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_8743716903167871370.key 925615 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 925724 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_9680538117969854902.key 925724 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_9680538117969854902.key 925724 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.2ns 925724 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 929601 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 929617 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_9680538117969854902.key 929617 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.3ns 929727 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4133975463013481751.key 929727 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4133975463013481751.key 929727 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.4ns 929727 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 933588 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 933604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_4133975463013481751.key 933604 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 933713 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_5661036063807092301.key 933713 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_5661036063807092301.key 933713 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.2ns 933713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 937590 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 937621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_5661036063807092301.key 937621 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 937731 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_752224201861407694.key 937731 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_752224201861407694.key 937731 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.6ns 937731 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 941670 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s 941686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_752224201861407694.key 941686 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 941795 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 941795 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 941795 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.6ns 941795 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 945783 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.99s 945798 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 945798 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms 945929 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_12665324198436902943.key 945929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_12665324198436902943.key 945929 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.2ns 945929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 949852 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s 949868 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_12665324198436902943.key 949884 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 949993 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_1213314876108462187.key 949993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_1213314876108462187.key 949993 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.9ns 949993 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 953917 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s 953948 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_1213314876108462187.key 953948 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 954058 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_16640166027235262866.key 954058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_16640166027235262866.key 954058 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.8ns 954058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 957983 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s 957999 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_16640166027235262866.key 957999 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 958108 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_14204585844710762517.key 958108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_14204585844710762517.key 958108 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.3ns 958108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 962032 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 962047 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_14204585844710762517.key 962047 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 962157 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14992823340439351396.key 962157 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14992823340439351396.key 962157 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 389.4ns 962157 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 966082 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 966098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_14992823340439351396.key 966098 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 966207 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9168815734071117771.key 966207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9168815734071117771.key 966207 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242ns 966207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 970116 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.91s 970131 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_9168815734071117771.key 970147 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 970256 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_9847246653910205331.key 970256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_9847246653910205331.key 970256 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243ns 970256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 974211 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.96s 974243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_9847246653910205331.key 974243 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 974352 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_7111622904750475639.key 974352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_7111622904750475639.key 974352 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.8ns 974352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 978823 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.47s 978838 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_7111622904750475639.key 978838 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 978948 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_2417653425229170928.key 978948 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_2417653425229170928.key 978948 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.2ns 978948 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 982746 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 982762 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_2417653425229170928.key 982762 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 982871 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_2640975390219392088.key 982871 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_2640975390219392088.key 982871 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235ns 982871 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 986688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.82s 986704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_2640975390219392088.key 986719 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 986829 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_14178072321104602613.key 986829 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_14178072321104602613.key 986829 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.3ns 986829 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 990643 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.81s 990659 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_14178072321104602613.key 990659 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 990768 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12558318776845633134.key 990768 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12558318776845633134.key 990768 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.7ns 990768 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 994537 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.77s 994553 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_12558318776845633134.key 994553 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 994662 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_5013824189996558688.key 994662 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_5013824189996558688.key 994662 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.1ns 994662 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 998429 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 998461 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_5013824189996558688.key 998461 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 998570 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_5782131513150183127.key 998570 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_5782131513150183127.key 998570 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.4ns 998570 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1002337 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.77s 1002353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_5782131513150183127.key 1002353 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns