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.815s | 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.799s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.797s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.755s | 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.761s | passed |
| [15] seqConcat.dl, \forall int i; \forall Seq s1; \forall Seq s2; ( 0 <= i & i < seqLen(s1) + seqLen(s2) -> any::seqGet(seqConcat(s1, s2), i) = \if (i < seqLen(s1)) \then (any::seqGet(s1, i)) \else (any::seqGet(s2, i-seqLen(s1)))) | testSMTLemmaSoundness(String, String)[15] | 2.776s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.971s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.735s | 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.720s | passed |
| [19] anon.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Heap h2; \forall LocSet ls; any::select(anon(h, ls, h2), o, f)<<Trigger>> = \if(elementOf(o, f, ls) & f != java.lang.Object::<created> | elementOf(o, f, freshLocs(h))) \then(any::select(h2, o, f)) \else(any::select(h, o, f)) | testSMTLemmaSoundness(String, String)[19] | 2.728s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.858s | 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.823s | 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.732s | passed |
| [22] seqSub.dl.2, \forall Seq seq; \forall int from; \forall int to; seqLen(seqSub(seq, from, to)<<Trigger>>) = \if(from < to)\then(to - from)\else(0) | testSMTLemmaSoundness(String, String)[22] | 2.744s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.735s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.712s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.729s | 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.856s | 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.907s | 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.830s | passed |
| [5] create.dl, \forall Heap h; \forall Object o; \forall Object o2; \forall Field f; any::select(create(h, o), o2, f)<<Trigger>> = \if(o = o2 & o != null & f = java.lang.Object::<created>) \then(TRUE) \else(any::select(h, o2, f)) | testSMTLemmaSoundness(String, String)[5] | 2.823s | 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.838s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.801s | 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.791s | 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.797s | passed |
Standard output
582497 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 582497 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 582498 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.4ns 582501 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 585208 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 585224 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 585239 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.47ms 585352 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_14832031847023583250.key 585352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_14832031847023583250.key 585352 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.7ns 585352 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 588083 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 588099 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_14832031847023583250.key 588099 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 588209 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 588209 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 588209 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.4ns 588209 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 590922 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 590937 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 591000 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.19ms 591117 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7765168295590064227.key 591117 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7765168295590064227.key 591117 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 461.1ns 591117 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 593823 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 593839 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_7765168295590064227.key 593839 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 593948 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10836514224519279129.key 593948 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10836514224519279129.key 593948 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.3ns 593948 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 596643 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 596659 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_10836514224519279129.key 596659 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 596771 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_11258941814883456145.key 596771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_11258941814883456145.key 596771 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.7ns 596771 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 599485 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 599485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_11258941814883456145.key 599501 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 599610 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_18048045492155717075.key 599610 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_18048045492155717075.key 599610 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 195ns 599610 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 602283 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 602299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_18048045492155717075.key 602299 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 602413 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_17983182532326726003.key 602413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_17983182532326726003.key 602413 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.5ns 602413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 605079 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 605079 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_17983182532326726003.key 605095 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 605204 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_11623616223970351209.key 605204 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_11623616223970351209.key 605204 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.6ns 605204 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 607862 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 607877 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_11623616223970351209.key 607877 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 218.7ns 608002 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6585959403104439932.key 608002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6585959403104439932.key 608002 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.8ns 608002 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 610688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 610704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_6585959403104439932.key 610704 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 610818 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 610818 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 610818 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 159ns 610818 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 613492 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 613492 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 613508 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.48ms 613617 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15282608498035215862.key 613617 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15282608498035215862.key 613617 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.1ns 613617 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 616290 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 616290 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_15282608498035215862.key 616305 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 616415 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_16484867379459265226.key 616415 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_16484867379459265226.key 616415 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.5ns 616415 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 619041 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 619057 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_16484867379459265226.key 619057 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 619170 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14376969667419660885.key 619170 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14376969667419660885.key 619170 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.6ns 619170 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 621807 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 621823 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_14376969667419660885.key 621823 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 621932 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15941537400169235105.key 621932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15941537400169235105.key 621932 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 621932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 624579 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 624595 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_15941537400169235105.key 624595 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 624709 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_1075529536120658065.key 624709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_1075529536120658065.key 624709 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.7ns 624709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 627322 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 627338 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_1075529536120658065.key 627338 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 627681 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_8597401460444461477.key 627681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_8597401460444461477.key 627681 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.8ns 627681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 630292 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 630308 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_8597401460444461477.key 630308 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 630417 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_1677479212665422973.key 630417 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_1677479212665422973.key 630417 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.6ns 630417 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 633012 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 633027 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_1677479212665422973.key 633027 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.2ns 633137 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15797727331676557869.key 633137 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15797727331676557869.key 633137 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.7ns 633137 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 635740 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 635755 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_15797727331676557869.key 635755 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 635865 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_6385222314764259690.key 635865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_6385222314764259690.key 635865 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.1ns 635865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 638493 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 638571 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_6385222314764259690.key 638571 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.4ns 638689 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_10236225798451810819.key 638689 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_10236225798451810819.key 638689 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.2ns 638689 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 641292 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 641308 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_10236225798451810819.key 641308 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 641421 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_3771885849595464756.key 641421 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_3771885849595464756.key 641421 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.5ns 641421 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 644037 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 644052 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_3771885849595464756.key 644052 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 644165 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_5128632639601525586.key 644165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_5128632639601525586.key 644165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.6ns 644165 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 646760 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 646775 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_5128632639601525586.key 646791 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 646900 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_12025989352638997852.key 646900 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_12025989352638997852.key 646900 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.9ns 646900 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 649484 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 649499 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_12025989352638997852.key 649499 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 649613 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12244151006218125729.key 649613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_12244151006218125729.key 649613 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225ns 649613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 652217 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 652233 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_12244151006218125729.key 652233 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns