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.285s | 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.285s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.752s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.720s | 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.256s | 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] | 5.333s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.313s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.286s | 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] | 5.175s | 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] | 5.216s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.321s | 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] | 5.285s | 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.238s | 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.221s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.221s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.254s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.268s | 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.347s | 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] | 5.378s | 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.315s | 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.424s | 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] | 5.299s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.316s | 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.269s | 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.302s | passed |
Standard output
1240929 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 1240929 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 1240929 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 1240929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1246104 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.17s 1246120 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1246135 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.64ms 1246245 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13597947387986324698.key 1246245 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13597947387986324698.key 1246245 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.2ns 1246245 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1251451 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.21s 1251482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_13597947387986324698.key 1251482 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 1251592 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 1251592 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 1251592 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.4ns 1251592 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1256798 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.21s 1256813 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1256861 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.33ms 1256970 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_8188824283657550592.key 1256970 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_8188824283657550592.key 1256970 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 177ns 1256970 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1262160 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s 1262176 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_8188824283657550592.key 1262176 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 1262285 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_5978761384799339351.key 1262285 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_5978761384799339351.key 1262285 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.6ns 1262285 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1267568 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s 1267584 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_5978761384799339351.key 1267584 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 1267709 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_5727200694182574540.key 1267709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_5727200694182574540.key 1267709 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.6ns 1267709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1272883 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.17s 1272899 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_5727200694182574540.key 1272899 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 1273008 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_18204582714425536811.key 1273008 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_18204582714425536811.key 1273008 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 440.3ns 1273008 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1278184 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s 1278215 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_18204582714425536811.key 1278215 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.4ns 1278324 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_5372384295211680776.key 1278324 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_5372384295211680776.key 1278324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.17ms 1278324 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1283468 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.14s 1283484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_5372384295211680776.key 1283484 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 1283593 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_15307604232181626398.key 1283593 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_15307604232181626398.key 1283593 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.5ns 1283593 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1288754 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s 1288785 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_15307604232181626398.key 1288785 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1288895 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4642266299473926048.key 1288895 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4642266299473926048.key 1288895 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.3ns 1288895 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1294039 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.15s 1294071 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_4642266299473926048.key 1294071 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 1294180 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 1294180 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 1294180 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.3ns 1294180 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1299324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.14s 1299339 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1299339 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 1299465 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_2327276525552611609.key 1299465 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_2327276525552611609.key 1299465 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.6ns 1299465 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1305076 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.61s 1305092 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_2327276525552611609.key 1305108 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 1305217 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_17024694349595295540.key 1305217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_17024694349595295540.key 1305217 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.8ns 1305217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1310797 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.58s 1310829 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_17024694349595295540.key 1310829 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 1310938 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_7669904114379126932.key 1310938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_7669904114379126932.key 1310938 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.8ns 1310938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1316054 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.11s 1316069 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_7669904114379126932.key 1316085 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 557.4ns 1316194 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12843747302369983422.key 1316194 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12843747302369983422.key 1316194 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.3ns 1316194 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1321402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 1321417 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_12843747302369983422.key 1321417 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1321527 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16542169994923130656.key 1321527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_16542169994923130656.key 1321527 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 397.4ns 1321527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1326716 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s 1326732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_16542169994923130656.key 1326732 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 1326841 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_11659856034099220329.key 1326841 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_11659856034099220329.key 1326841 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.5ns 1326841 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1332002 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.15s 1332018 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_11659856034099220329.key 1332018 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1332127 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_4535719606547010895.key 1332127 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_4535719606547010895.key 1332127 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.2ns 1332127 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1337177 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.05s 1337193 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_4535719606547010895.key 1337193 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 1337302 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_1701403229028908022.key 1337302 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_1701403229028908022.key 1337302 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.9ns 1337302 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1342393 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.09s 1342409 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_1701403229028908022.key 1342409 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 1342518 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_15444540916560460627.key 1342518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_15444540916560460627.key 1342518 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.9ns 1342518 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1347678 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.15s 1347694 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_15444540916560460627.key 1347694 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ns 1347803 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7882129567520348078.key 1347803 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7882129567520348078.key 1347803 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.6ns 1347803 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1352900 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 1352916 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_7882129567520348078.key 1352916 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 1353041 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_14023940287696399738.key 1353041 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_14023940287696399738.key 1353041 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 458.1ns 1353041 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1358137 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.09s 1358152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_14023940287696399738.key 1358152 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1358262 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_14916572233969725672.key 1358262 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_14916572233969725672.key 1358262 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.6ns 1358262 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1363342 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.08s 1363374 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_14916572233969725672.key 1363374 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 1363483 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_8141342050391514765.key 1363483 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_8141342050391514765.key 1363483 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.8ns 1363483 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1368611 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.13s 1368626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_8141342050391514765.key 1368626 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 1368737 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_11501563621450220024.key 1368737 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_11501563621450220024.key 1368737 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.9ns 1368737 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1373880 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.14s 1373896 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_11501563621450220024.key 1373896 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns