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] | 5.058s | 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] | 5.002s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.977s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.975s | 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] | 5.000s | 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.856s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.980s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.035s | 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.969s | 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.942s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.132s | 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.982s | 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] | 5.019s | 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] | 5.028s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.932s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.925s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.988s | 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] | 5.079s | 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.989s | 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] | 5.043s | 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] | 5.028s | 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.926s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.032s | 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] | 5.077s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 5.042s | passed |
Standard output
1128130 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 1128130 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 1128130 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.1ns 1128130 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1133126 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.99s 1133141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1133141 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 1133251 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_2939669104469330160.key 1133251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_2939669104469330160.key 1133251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.6ns 1133251 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1138203 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 1138218 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_2939669104469330160.key 1138218 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1138330 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 1138330 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 1138330 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.3ns 1138330 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1143163 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.83s 1143179 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1143210 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.11ms 1143320 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_18300105985132194539.key 1143320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_18300105985132194539.key 1143320 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.6ns 1143320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1148238 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 1148253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_18300105985132194539.key 1148253 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.6ns 1148363 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_2450536610678226003.key 1148363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_2450536610678226003.key 1148363 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.5ns 1148363 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1153262 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s 1153277 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_2450536610678226003.key 1153277 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1153391 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_1291599265857074579.key 1153391 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_1291599265857074579.key 1153391 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.4ns 1153391 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1158186 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.8s 1158202 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_1291599265857074579.key 1158202 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 1158317 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_16101987129994368342.key 1158317 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_16101987129994368342.key 1158317 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230ns 1158317 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1163224 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s 1163240 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_16101987129994368342.key 1163240 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1163349 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3357551465546900539.key 1163349 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3357551465546900539.key 1163349 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.8ns 1163349 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1168301 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 1168316 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_3357551465546900539.key 1168316 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1168426 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_1805535841061969386.key 1168426 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_1805535841061969386.key 1168426 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.1ns 1168426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1173327 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 1173358 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_1805535841061969386.key 1173358 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1173468 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_11882803629169695583.key 1173468 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_11882803629169695583.key 1173468 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.6ns 1173468 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1178398 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.93s 1178414 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_11882803629169695583.key 1178414 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1178527 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 1178527 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 1178527 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.6ns 1178527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1183388 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.87s 1183404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1183420 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 1183529 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14009934019136565563.key 1183529 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_14009934019136565563.key 1183529 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.9ns 1183529 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1188365 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.84s 1188381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_14009934019136565563.key 1188396 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1188506 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_604170370224768063.key 1188506 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_604170370224768063.key 1188506 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.4ns 1188506 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1193356 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.85s 1193372 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_604170370224768063.key 1193372 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1193481 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9411426338524946741.key 1193481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9411426338524946741.key 1193481 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.3ns 1193481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1198355 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.87s 1198371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_9411426338524946741.key 1198371 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1198481 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12367381048030214096.key 1198481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12367381048030214096.key 1198481 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.9ns 1198481 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1203212 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.73s 1203228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_12367381048030214096.key 1203228 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1203337 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10603927789490007748.key 1203337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_10603927789490007748.key 1203337 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.7ns 1203337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1208189 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.85s 1208205 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_10603927789490007748.key 1208205 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 1208318 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_10263456022289488342.key 1208318 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_10263456022289488342.key 1208318 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.8ns 1208318 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1213226 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 1213242 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_10263456022289488342.key 1213242 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 1213353 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_13769980851135080011.key 1213353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_13769980851135080011.key 1213353 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.7ns 1213353 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1218165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.81s 1218212 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_13769980851135080011.key 1218212 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ns 1218322 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8836481779247282690.key 1218322 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8836481779247282690.key 1218322 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.2ns 1218322 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1223135 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.81s 1223151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_8836481779247282690.key 1223151 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1223264 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_226946885062470501.key 1223264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_226946885062470501.key 1223264 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.1ns 1223264 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1228105 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.85s 1228136 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_226946885062470501.key 1228136 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1228246 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_16625946274368505693.key 1228246 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_16625946274368505693.key 1228246 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244ns 1228246 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1233138 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 1233153 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_16625946274368505693.key 1233153 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1233265 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_8825250495964382711.key 1233265 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_8825250495964382711.key 1233265 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.4ns 1233265 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1238168 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s 1238183 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_8825250495964382711.key 1238183 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ns 1238293 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6622149665080657847.key 1238293 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6622149665080657847.key 1238293 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.3ns 1238293 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1243095 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.8s 1243111 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_6622149665080657847.key 1243111 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1243225 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_12175697279759510471.key 1243225 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_12175697279759510471.key 1243225 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.1ns 1243225 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1248021 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.8s 1248037 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_12175697279759510471.key 1248037 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1248151 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6410765424422419044.key 1248151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6410765424422419044.key 1248151 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.1ns 1248151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1253013 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s 1253029 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_6410765424422419044.key 1253029 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns