ProveSMTLemmasTest
|
100%
successful |
Tests
| Test | Method name | Duration | Result |
|---|---|---|---|
| [10] wellFormed.dl, \forall Heap h; \forall Object o; \forall Field f; (wellFormed(h) -> boolean::select(h, (java.lang.Object::select(h, o, f))<<Trigger>>, java.lang.Object::<created>) = TRUE | (java.lang.Object::select(h, o, f)) = null) | testSMTLemmaSoundness(String, String)[10] | 3.628s | passed |
| [11] jdiv.dl, \forall int divNum; \forall int divDenom; jdiv(divNum,divDenom) = \if (divNum >= 0) \then (div(divNum,divDenom)) \else (div(divNum*(-1),divDenom)*(-1)) | testSMTLemmaSoundness(String, String)[11] | 3.611s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.501s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.550s | passed |
| [14] arrayRange.dl, \forall Object o; \forall Object o2; \forall Field f; \forall int lo; \forall int hi; (elementOf(o,f, arrayRange(o2, lo, hi))<<Trigger>> <-> o = o2 & \exists int iv; (f = arr(iv) & lo <= iv & iv <= hi)) | testSMTLemmaSoundness(String, String)[14] | 3.595s | 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.566s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.642s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.627s | passed |
| [18] freshLocs.dl, \forall Heap h; \forall Object o; \forall Field f; ( elementOf(o,f,freshLocs(h))<<Trigger>> <-> o != null & !boolean::select(h,o,java.lang.Object::<created>)=TRUE ) | testSMTLemmaSoundness(String, String)[18] | 3.595s | 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.519s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.799s | 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.549s | 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.611s | 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.754s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.596s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.861s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.580s | passed |
| [2] seqSub.dl, \forall Seq seq; \forall int from; \forall int to; \forall int idx; any::seqGet(seqSub(seq, from, to)<<Trigger>>, idx) = \if(0 <= idx & idx < (to - from)) \then(any::seqGet(seq, idx + from)) \else(seqGetOutside) | testSMTLemmaSoundness(String, String)[2] | 3.784s | passed |
| [3] seqGetOutside.dl, \forall int i; \forall Seq s; ( i < 0 | i >= seqLen(s) -> any::seqGet(s, i)<<Trigger>> = seqGetOutside ) | testSMTLemmaSoundness(String, String)[3] | 3.659s | passed |
| [4] singleton.dl, \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; ( elementOf(o,f, singleton(o2,f2))<<Trigger>> <-> o = o2 & f = f2 ) | testSMTLemmaSoundness(String, String)[4] | 3.768s | 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.736s | passed |
| [6] allFields.dl, \forall Object o; \forall Field f; \forall Object o2; ( elementOf(o,f, allFields(o2))<<Trigger>> <-> o = o2 ) | testSMTLemmaSoundness(String, String)[6] | 3.657s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.737s | 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.628s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 3.565s | passed |
Standard output
866118 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 866118 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 866118 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.2ns 866118 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 869792 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.67s 869808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 869808 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.43ms 869917 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17730894506850763561.key 869917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17730894506850763561.key 869917 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.7ns 869917 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 873576 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 873592 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_17730894506850763561.key 873592 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 873701 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 873701 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 873701 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.7ns 873701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 877204 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 877219 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 877251 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.47ms 877360 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7521334384662148662.key 877360 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_7521334384662148662.key 877360 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.4ns 877360 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 880987 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s 881003 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_7521334384662148662.key 881018 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 508.4ns 881128 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_6389582021471097833.key 881128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_6389582021471097833.key 881128 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.1ns 881128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 884739 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 884755 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_6389582021471097833.key 884755 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 884864 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_2100099749471161978.key 884864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_2100099749471161978.key 884864 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.6ns 884864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 888381 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 888413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_2100099749471161978.key 888413 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 888522 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_12099675402082468907.key 888522 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_12099675402082468907.key 888522 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.1ns 888522 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 892134 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 892149 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_12099675402082468907.key 892149 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 892259 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_5246386866931845721.key 892259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_5246386866931845721.key 892259 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.8ns 892259 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 895746 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 895777 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_5246386866931845721.key 895777 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 895887 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_11171146820216938280.key 895887 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_11171146820216938280.key 895887 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 203ns 895887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 899326 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 899342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_11171146820216938280.key 899342 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 899452 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_7490638547231485403.key 899452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_7490638547231485403.key 899452 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.9ns 899452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 902939 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 902970 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_7490638547231485403.key 902970 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 903080 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 903080 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 903080 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.5ns 903080 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 906519 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 906581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 906581 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 906691 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5467517804254732120.key 906691 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_5467517804254732120.key 906691 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.5ns 906691 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 910067 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 910083 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_5467517804254732120.key 910083 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 910192 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_7803255092359986346.key 910192 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_7803255092359986346.key 910192 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 306ns 910192 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 913617 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 913632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_7803255092359986346.key 913632 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 913742 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11969785087673617352.key 913742 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11969785087673617352.key 913742 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.7ns 913742 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 917181 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 917228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_11969785087673617352.key 917228 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 917337 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_17952594603500151634.key 917337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_17952594603500151634.key 917337 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 261ns 917337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 920762 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 920793 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_17952594603500151634.key 920793 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 920903 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_3995902763924402509.key 920903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_3995902763924402509.key 920903 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.1ns 920903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 924421 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 924437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_3995902763924402509.key 924437 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 924546 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2089107724172494579.key 924546 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2089107724172494579.key 924546 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 402ns 924546 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 928033 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 928064 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_2089107724172494579.key 928064 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 928173 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_8367952713393296876.key 928173 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_8367952713393296876.key 928173 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.4ns 928173 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 931628 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 931659 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_8367952713393296876.key 931659 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.2ns 931768 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_10318874048365507579.key 931768 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_10318874048365507579.key 931768 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.1ns 931768 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 935146 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 935178 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_10318874048365507579.key 935178 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 935287 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_8664938585733907831.key 935287 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_8664938585733907831.key 935287 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 553.4ns 935287 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 938711 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 938726 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_8664938585733907831.key 938726 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 938836 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_12110239780728003345.key 938836 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_12110239780728003345.key 938836 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.1ns 938836 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 942322 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 942338 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_12110239780728003345.key 942338 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 942447 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_5577869546934561543.key 942447 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_5577869546934561543.key 942447 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.4ns 942447 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 946076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s 946091 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_5577869546934561543.key 946091 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 946201 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_8230830542176514245.key 946201 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_8230830542176514245.key 946201 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.1ns 946201 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 949672 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 949688 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_8230830542176514245.key 949688 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 949797 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_4971357598489434845.key 949797 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_4971357598489434845.key 949797 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.3ns 949797 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 953533 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 953549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_4971357598489434845.key 953549 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 953658 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_18020485759263451493.key 953658 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_18020485759263451493.key 953658 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.2ns 953658 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 957097 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 957128 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_18020485759263451493.key 957128 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns