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.385s | 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.030s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.686s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.119s | 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.049s | 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.302s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.066s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.085s | 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.227s | 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.032s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.067s | 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.261s | 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.028s | 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.081s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.336s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.058s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.049s | 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.320s | 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.364s | 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.177s | 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.434s | 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.101s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.321s | 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.120s | 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.129s | passed |
Standard output
1180365 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 1180365 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 1180365 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 1180365 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1185266 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s 1185297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1185304 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.79ms 1185424 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17808595167833632496.key 1185424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17808595167833632496.key 1185424 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.2ns 1185424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1190612 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.19s 1190628 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_17808595167833632496.key 1190628 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1190744 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 1190744 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 1190744 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 215ns 1190744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1195943 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 1195959 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1195990 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.25ms 1196108 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_1639110404875760316.key 1196108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_1639110404875760316.key 1196108 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.1ns 1196108 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1201159 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.04s 1201174 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_1639110404875760316.key 1201174 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1201285 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14212007872563147799.key 1201285 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_14212007872563147799.key 1201285 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.8ns 1201285 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1206589 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.3s 1206604 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_14212007872563147799.key 1206604 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.1ns 1206720 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_4786054940052766732.key 1206720 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_4786054940052766732.key 1206720 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.8ns 1206720 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1211691 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 1211707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_4786054940052766732.key 1211707 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1211821 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_16365454389306990153.key 1211821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_16365454389306990153.key 1211821 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.8ns 1211821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1217006 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s 1217022 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_16365454389306990153.key 1217022 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 1217145 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6849824254324996022.key 1217145 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6849824254324996022.key 1217145 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.8ns 1217145 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1222135 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.99s 1222151 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_6849824254324996022.key 1222151 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1222262 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_14657674721450753231.key 1222262 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_14657674721450753231.key 1222262 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 177ns 1222262 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1227250 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.99s 1227266 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_14657674721450753231.key 1227282 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1227391 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_15975392006487501920.key 1227391 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_15975392006487501920.key 1227391 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.2ns 1227391 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1232647 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.25s 1232663 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_15975392006487501920.key 1232663 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1232778 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 1232778 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 1232778 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.5ns 1232778 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1237666 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 1237697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1237697 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 1237808 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_13131421565190155428.key 1237808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_13131421565190155428.key 1237808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.8ns 1237808 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1243365 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.55s 1243381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_13131421565190155428.key 1243381 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1243495 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13005579672302515790.key 1243495 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_13005579672302515790.key 1243495 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.1ns 1243495 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1248475 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1248506 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_13005579672302515790.key 1248506 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 1248615 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17305559001372017173.key 1248615 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_17305559001372017173.key 1248615 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.4ns 1248615 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1253485 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s 1253547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_17305559001372017173.key 1253547 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1253664 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_3445662075518461038.key 1253664 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_3445662075518461038.key 1253664 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.8ns 1253664 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1258839 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.17s 1258854 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_3445662075518461038.key 1258854 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1258967 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14474637695244310484.key 1258967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14474637695244310484.key 1258967 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.5ns 1258967 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1263907 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.93s 1263923 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_14474637695244310484.key 1263923 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1264034 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2443624918344536160.key 1264034 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2443624918344536160.key 1264034 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.3ns 1264034 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1268990 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 1269006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_2443624918344536160.key 1269006 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 1269119 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_16819680243599913278.key 1269119 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_16819680243599913278.key 1269119 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 486.9ns 1269119 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1274206 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.09s 1274221 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_16819680243599913278.key 1274221 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.8ns 1274347 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2081364338394932674.key 1274347 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_2081364338394932674.key 1274347 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.1ns 1274347 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1279253 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s 1279269 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_2081364338394932674.key 1279269 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.4ns 1279379 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_194901475020571260.key 1279379 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_194901475020571260.key 1279379 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.6ns 1279379 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1284515 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.13s 1284531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_194901475020571260.key 1284531 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1284640 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7863664945576280444.key 1284640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7863664945576280444.key 1284640 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.7ns 1284640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1289529 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 1289544 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_7863664945576280444.key 1289544 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1289669 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_5019351969873199482.key 1289669 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_5019351969873199482.key 1289669 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.5ns 1289669 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1294619 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 1294634 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_5019351969873199482.key 1294634 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1294750 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_18062817665274809147.key 1294750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_18062817665274809147.key 1294750 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.7ns 1294750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1299962 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 1299978 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_18062817665274809147.key 1299978 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 1300087 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_3837210703341017744.key 1300087 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_3837210703341017744.key 1300087 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.5ns 1300087 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1305023 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.93s 1305039 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_3837210703341017744.key 1305039 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1305148 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_17419469932456247536.key 1305148 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_17419469932456247536.key 1305148 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 163ns 1305148 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1310057 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 1310073 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_17419469932456247536.key 1310073 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.6ns