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.657s | 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.594s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.580s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.611s | 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.580s | 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.673s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.671s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.579s | 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.610s | 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.578s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.616s | 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.595s | 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.604s | 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.642s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.705s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.697s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.626s | 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.723s | 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.658s | 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.643s | 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.720s | 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.626s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.752s | 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.610s | 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.610s | passed |
Standard output
642943 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 642943 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 642943 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 642943 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 645444 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 645459 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 645459 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 645569 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8297432299248246748.key 645569 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_8297432299248246748.key 645569 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.8ns 645569 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 648164 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 648180 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_8297432299248246748.key 648180 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ns 648289 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 648289 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 648289 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.3ns 648289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 650791 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 650807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 650838 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.04ms 650948 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_584488081786728864.key 650948 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_584488081786728864.key 650948 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.2ns 650948 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 653480 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 653480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_584488081786728864.key 653480 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ns 653590 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_11007409194301074966.key 653590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_11007409194301074966.key 653590 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.8ns 653590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 656185 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 656200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_11007409194301074966.key 656200 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ns 656310 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_15215236198151407984.key 656310 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_15215236198151407984.key 656310 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.6ns 656310 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 658811 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 658827 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_15215236198151407984.key 658827 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ns 658936 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2867740937599034722.key 658936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2867740937599034722.key 658936 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 184ns 658936 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 661485 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 661579 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_2867740937599034722.key 661579 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ns 661688 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15188671464072249242.key 661688 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_15188671464072249242.key 661688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.3ns 661688 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 664174 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 664189 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_15188671464072249242.key 664189 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.3ns 664299 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_9477763817176086568.key 664299 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_9477763817176086568.key 664299 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 186ns 664299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 666784 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 666800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_9477763817176086568.key 666800 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ns 666909 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_11234763938050534635.key 666909 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_11234763938050534635.key 666909 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.5ns 666909 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 669442 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 669442 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_11234763938050534635.key 669442 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ns 669567 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 669567 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 669567 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.7ns 669567 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 672037 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 672052 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 672052 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 672162 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_9620100648848702116.key 672162 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_9620100648848702116.key 672162 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185ns 672162 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 674617 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 674633 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_9620100648848702116.key 674633 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 674742 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_14476042983671118601.key 674742 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_14476042983671118601.key 674742 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.2ns 674742 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 677229 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 677244 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_14476042983671118601.key 677244 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ns 677354 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9201647024071567190.key 677354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9201647024071567190.key 677354 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.6ns 677354 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 679809 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 679824 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_9201647024071567190.key 679824 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ns 679934 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_14856023066221760001.key 679934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_14856023066221760001.key 679934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.9ns 679934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 682483 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 682498 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_14856023066221760001.key 682498 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 682608 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13568725210169736040.key 682608 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13568725210169736040.key 682608 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.6ns 682608 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 685172 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 685172 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_13568725210169736040.key 685172 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.1ns 685281 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_1850349276840387994.key 685281 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_1850349276840387994.key 685281 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.9ns 685281 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 687736 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 687751 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_1850349276840387994.key 687751 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 687861 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_1137129148472146589.key 687861 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_1137129148472146589.key 687861 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 184ns 687861 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 690347 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 690362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_1137129148472146589.key 690362 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 690471 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_18337586223753701705.key 690471 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_18337586223753701705.key 690471 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.3ns 690471 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 692925 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 692941 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_18337586223753701705.key 692941 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ns 693050 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_5812874244552034484.key 693050 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_5812874244552034484.key 693050 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.2ns 693050 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 695520 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 695535 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_5812874244552034484.key 695535 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ns 695645 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_17941507164736084950.key 695645 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_17941507164736084950.key 695645 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.9ns 695645 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 698130 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 698146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_17941507164736084950.key 698146 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 698250 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_10486441547965151142.key 698250 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_10486441547965151142.key 698250 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.1ns 698250 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 700767 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 700783 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_10486441547965151142.key 700783 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ns 700892 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12696202931159412902.key 700892 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_12696202931159412902.key 700892 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.8ns 700892 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 703472 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 703487 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_12696202931159412902.key 703487 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.6ns 703598 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_5794252227333586357.key 703598 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_5794252227333586357.key 703598 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.2ns 703598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 706177 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 706193 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_5794252227333586357.key 706193 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ns 706302 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3781780555795066573.key 706302 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3781780555795066573.key 706302 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.3ns 706302 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 708804 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 708804 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_3781780555795066573.key 708819 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ns