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.584s | 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.665s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.488s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.566s | 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.520s | 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.612s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.549s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.580s | 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.690s | 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.503s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.548s | 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] | 4.488s | 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] | 4.486s | 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] | 4.566s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.551s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.410s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.532s | 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.581s | 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.519s | 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.472s | 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.378s | 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.468s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.550s | 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] | 4.379s | 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.439s | passed |
Standard output
993664 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 993664 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 993664 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.7ns 993664 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 998074 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.41s 998105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 998105 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.15ms 998214 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_2266710009058518246.key 998214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_2266710009058518246.key 998214 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.5ns 998214 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1002670 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.45s 1002686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_2266710009058518246.key 1002686 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 1002795 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 1002795 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 1002795 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 460ns 1002795 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1007158 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.36s 1007189 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1007205 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.72ms 1007314 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_5409470883142880357.key 1007314 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_5409470883142880357.key 1007314 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.1ns 1007314 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1011645 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s 1011660 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_5409470883142880357.key 1011676 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 1011786 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14944957510275314433.key 1011786 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14944957510275314433.key 1011786 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.5ns 1011786 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1016007 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.21s 1016039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_14944957510275314433.key 1016054 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 1016164 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_14091556144749118653.key 1016164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_14091556144749118653.key 1016164 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 284ns 1016164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1020507 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.34s 1020523 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_14091556144749118653.key 1020523 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 1020632 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_443556452219138154.key 1020632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_443556452219138154.key 1020632 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.7ns 1020632 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1025057 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.42s 1025072 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_443556452219138154.key 1025072 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.9ns 1025182 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_17751992417912136.key 1025182 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_17751992417912136.key 1025182 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.1ns 1025182 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1029420 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1029451 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_17751992417912136.key 1029451 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1029561 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_331297809636178635.key 1029561 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_331297809636178635.key 1029561 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.9ns 1029561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1033875 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.31s 1033890 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_331297809636178635.key 1033890 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 1034000 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4541632523521207473.key 1034000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4541632523521207473.key 1034000 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.8ns 1034000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1038443 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.45s 1038475 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_4541632523521207473.key 1038475 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 1038584 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 1038584 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 1038584 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 603.9ns 1038584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1043108 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.53s 1043139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1043139 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.09ms 1043249 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_4852543900654441182.key 1043249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_4852543900654441182.key 1043249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 450.8ns 1043249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1047595 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 1047627 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_4852543900654441182.key 1047627 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 1047739 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_10393139122462745353.key 1047739 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_10393139122462745353.key 1047739 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.8ns 1047739 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1052162 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.43s 1052178 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_10393139122462745353.key 1052178 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 1052303 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_70583438266352014.key 1052303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_70583438266352014.key 1052303 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.4ns 1052303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1056698 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.39s 1056713 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_70583438266352014.key 1056713 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 1056823 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_4592027496077221211.key 1056823 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_4592027496077221211.key 1056823 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.1ns 1056823 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1061294 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.47s 1061310 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_4592027496077221211.key 1061325 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 1061435 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_7314216338379802141.key 1061435 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_7314216338379802141.key 1061435 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.7ns 1061435 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1065844 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.42s 1065875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_7314216338379802141.key 1065875 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1065985 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_11801966008111488146.key 1065985 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_11801966008111488146.key 1065985 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.5ns 1065985 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1070425 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.44s 1070441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_11801966008111488146.key 1070456 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1070566 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_12044792849221840139.key 1070566 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_12044792849221840139.key 1070566 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.3ns 1070566 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1075115 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.56s 1075147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_12044792849221840139.key 1075147 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1075256 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_16041957378102722452.key 1075256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_16041957378102722452.key 1075256 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.9ns 1075256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1079634 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.38s 1079650 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_16041957378102722452.key 1079650 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 1079759 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14969781330067659596.key 1079759 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14969781330067659596.key 1079759 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.8ns 1079759 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1084106 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 1084138 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_14969781330067659596.key 1084138 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 1084247 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_13939675931753062942.key 1084247 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_13939675931753062942.key 1084247 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.5ns 1084247 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1088608 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.36s 1088624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_13939675931753062942.key 1088624 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 1088733 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_1754817145847112864.key 1088733 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_1754817145847112864.key 1088733 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 423.3ns 1088733 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1093174 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.44s 1093189 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_1754817145847112864.key 1093189 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1093299 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15136364233707033246.key 1093299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15136364233707033246.key 1093299 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.7ns 1093299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1097725 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.42s 1097741 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_15136364233707033246.key 1097741 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 1097857 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_15072756148047133484.key 1097857 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_15072756148047133484.key 1097857 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.8ns 1097857 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1102135 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.27s 1102150 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_15072756148047133484.key 1102150 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 1102260 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_2286773162690751987.key 1102260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_2286773162690751987.key 1102260 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.3ns 1102260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1106669 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.4s 1106685 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_2286773162690751987.key 1106685 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns