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.413s | 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.400s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.382s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.377s | 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.313s | 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.365s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.355s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.313s | 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.319s | 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.268s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.482s | 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.305s | 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.345s | 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.351s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.363s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.324s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.372s | 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.361s | 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.492s | 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.417s | 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.383s | 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.391s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.365s | 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.380s | 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.399s | passed |
Standard output
990064 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 990064 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 990064 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.1ns 990064 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 994408 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.34s 994424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 994439 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.49ms 994549 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_11477230389552028835.key 994549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_11477230389552028835.key 994549 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.8ns 994549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 998780 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 998796 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_11477230389552028835.key 998796 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 998910 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 998910 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 998910 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.8ns 998910 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1003214 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.31s 1003230 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1003292 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.04ms 1003402 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_18322644283299368338.key 1003402 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_18322644283299368338.key 1003402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.1ns 1003402 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1007692 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s 1007707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_18322644283299368338.key 1007707 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1007819 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_15808956459887797220.key 1007819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_15808956459887797220.key 1007819 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.5ns 1007819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1012076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1012091 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_15808956459887797220.key 1012091 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1012202 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_13058502325589402446.key 1012202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_13058502325589402446.key 1012202 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.6ns 1012202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1016462 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.26s 1016477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_13058502325589402446.key 1016477 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1016593 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6081503881515149851.key 1016593 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6081503881515149851.key 1016593 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.1ns 1016593 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1020827 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 1020843 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_6081503881515149851.key 1020843 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 1020958 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13013154301474532852.key 1020958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13013154301474532852.key 1020958 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 532.2ns 1020958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1025206 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1025222 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_13013154301474532852.key 1025222 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 1025338 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_17496581981338049779.key 1025338 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_17496581981338049779.key 1025338 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.6ns 1025338 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1029606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.27s 1029622 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_17496581981338049779.key 1029622 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1029737 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_687416980009179610.key 1029737 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_687416980009179610.key 1029737 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.9ns 1029737 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1034025 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 1034040 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_687416980009179610.key 1034040 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1034150 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 1034150 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 1034150 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.1ns 1034150 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1038417 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.27s 1038433 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1038433 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 1038550 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_12238783044978940261.key 1038550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_12238783044978940261.key 1038550 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.8ns 1038550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1042804 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1042819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_12238783044978940261.key 1042819 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.8ns 1042932 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8450340648876237365.key 1042932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8450340648876237365.key 1042932 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.3ns 1042932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1047187 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1047203 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_8450340648876237365.key 1047203 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1047309 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9593090173790266064.key 1047309 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9593090173790266064.key 1047309 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.2ns 1047309 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1051493 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 1051509 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_9593090173790266064.key 1051509 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1051622 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_13083292237826309878.key 1051622 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_13083292237826309878.key 1051622 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.8ns 1051622 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1055860 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 1055876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_13083292237826309878.key 1055876 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1055987 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_3055948005785366333.key 1055987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_3055948005785366333.key 1055987 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.9ns 1055987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1060212 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 1060228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_3055948005785366333.key 1060228 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1060343 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_12054388858748741843.key 1060343 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_12054388858748741843.key 1060343 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.8ns 1060343 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1064531 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 1064547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_12054388858748741843.key 1064547 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 1064656 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15230622623482676378.key 1064656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15230622623482676378.key 1064656 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.6ns 1064656 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1068844 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s 1068860 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_15230622623482676378.key 1068860 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ns 1068975 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15930346022437771241.key 1068975 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15930346022437771241.key 1068975 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.4ns 1068975 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1073118 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 1073133 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_15930346022437771241.key 1073133 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1073243 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_17744673975609991120.key 1073243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_17744673975609991120.key 1073243 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.3ns 1073243 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1077421 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 1077437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_17744673975609991120.key 1077437 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 1077548 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1344098163294466302.key 1077548 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1344098163294466302.key 1077548 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.6ns 1077548 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1081768 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 1081783 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_1344098163294466302.key 1081783 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ns 1081893 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_1171665830075900372.key 1081893 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_1171665830075900372.key 1081893 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.1ns 1081893 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1086119 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 1086135 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_1171665830075900372.key 1086135 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1086244 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_4632377913648229621.key 1086244 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_4632377913648229621.key 1086244 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.8ns 1086244 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1090475 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 1090491 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_4632377913648229621.key 1090491 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 1090607 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_4531319098310250431.key 1090607 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_4531319098310250431.key 1090607 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.3ns 1090607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1094804 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.2s 1094819 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_4531319098310250431.key 1094819 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1094932 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_13975245358256515509.key 1094932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_13975245358256515509.key 1094932 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 433.2ns 1094932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1099176 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 1099192 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_13975245358256515509.key 1099192 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns