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] | 3.908s | 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] | 3.940s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.923s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.877s | 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] | 3.863s | 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] | 3.893s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.910s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.908s | 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] | 3.924s | 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] | 3.877s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.988s | 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] | 3.971s | 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.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] | 3.924s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.908s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.878s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.893s | 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] | 3.971s | 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.080s | 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] | 3.940s | 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] | 3.861s | 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] | 3.927s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.907s | 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] | 3.893s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 3.910s | passed |
Standard output
919440 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 919440 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 919440 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.3ns 919440 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 923270 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.83s 923286 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 923302 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.68ms 923411 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_7879262560876994284.key 923411 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_7879262560876994284.key 923411 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.3ns 923411 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 927242 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.83s 927257 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_7879262560876994284.key 927273 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 927382 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 927382 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 927382 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.9ns 927382 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 931321 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s 931337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 931353 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.63ms 931462 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_1245068329455931367.key 931462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_1245068329455931367.key 931462 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.1ns 931462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 935261 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s 935293 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_1245068329455931367.key 935293 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 935402 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_2049258738055796827.key 935402 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_2049258738055796827.key 935402 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.3ns 935402 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 939138 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 939154 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_2049258738055796827.key 939154 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 939263 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_2083206484314910496.key 939263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_2083206484314910496.key 939263 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.9ns 939263 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 943049 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 943080 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_2083206484314910496.key 943080 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 943190 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_15494188303220242243.key 943190 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_15494188303220242243.key 943190 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.1ns 943190 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 946958 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.77s 946989 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_15494188303220242243.key 946989 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 947098 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6888479370561241117.key 947098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_6888479370561241117.key 947098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.7ns 947098 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 950850 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s 950866 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_6888479370561241117.key 950866 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 950991 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_12422963761941720508.key 950991 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_12422963761941720508.key 950991 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 240ns 950991 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 954775 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 954792 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_12422963761941720508.key 954792 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 954901 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4090130093059378350.key 954901 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_4090130093059378350.key 954901 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.5ns 954901 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 958683 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 958699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_4090130093059378350.key 958699 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 958809 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 958809 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 958809 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.3ns 958809 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 962609 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s 962624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 962640 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 962749 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15065019370793420753.key 962749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15065019370793420753.key 962749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.4ns 962749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 966501 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s 966563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_15065019370793420753.key 966563 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 966673 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_3790600429917245052.key 966673 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_3790600429917245052.key 966673 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.7ns 966673 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 970425 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s 970441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_3790600429917245052.key 970441 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 970550 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_12481254141881775075.key 970550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_12481254141881775075.key 970550 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.6ns 970550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 974288 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 974304 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_12481254141881775075.key 974304 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 974413 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_4023052667241325941.key 974413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_4023052667241325941.key 974413 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.8ns 974413 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 978165 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.76s 978196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_4023052667241325941.key 978196 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 978306 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_15825246451935862956.key 978306 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_15825246451935862956.key 978306 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.4ns 978306 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 982074 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.76s 982090 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_15825246451935862956.key 982105 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 982217 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6201711334699964526.key 982217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6201711334699964526.key 982217 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.4ns 982217 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 986000 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 986016 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_6201711334699964526.key 986016 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 986125 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_1706889139109966403.key 986125 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_1706889139109966403.key 986125 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256ns 986125 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 989924 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 989939 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_1706889139109966403.key 989939 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 990049 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_17290768975709143613.key 990049 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_17290768975709143613.key 990049 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.8ns 990049 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 993800 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s 993816 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_17290768975709143613.key 993816 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 993926 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13089427224468612528.key 993926 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13089427224468612528.key 993926 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.2ns 993926 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 997756 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.83s 997787 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_13089427224468612528.key 997787 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 997897 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_15702394309635554034.key 997897 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_15702394309635554034.key 997897 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.2ns 997897 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1001775 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 1001806 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_15702394309635554034.key 1001806 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 1001916 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_3818152846902663698.key 1001916 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_3818152846902663698.key 1001916 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.3ns 1001916 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1005699 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 1005730 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_3818152846902663698.key 1005730 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 1005840 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_16115934434899621727.key 1005840 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_16115934434899621727.key 1005840 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.7ns 1005840 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1009623 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 1009638 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_16115934434899621727.key 1009638 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 1009748 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_4945644372715866585.key 1009748 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_4945644372715866585.key 1009748 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.5ns 1009748 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1013485 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.74s 1013516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_4945644372715866585.key 1013516 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 1013626 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_14268145166850038781.key 1013626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_14268145166850038781.key 1013626 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244ns 1013626 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1017378 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s 1017394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_14268145166850038781.key 1017409 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns