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.925s | 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.924s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.926s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.940s | 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.956s | 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.909s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.940s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.955s | 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.955s | 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.988s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.999s | 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.939s | 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] | 3.941s | 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.940s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.938s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.956s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.956s | passed |
| [2] seqSub.dl, \forall Seq seq; \forall int from; \forall int to; \forall int idx; any::seqGet(seqSub(seq, from, to)<<Trigger>>, idx) = \if(0 <= idx & idx < (to - from)) \then(any::seqGet(seq, idx + from)) \else(seqGetOutside) | testSMTLemmaSoundness(String, String)[2] | 4.034s | 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.018s | passed |
| [4] singleton.dl, \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; ( elementOf(o,f, singleton(o2,f2))<<Trigger>> <-> o = o2 & f = f2 ) | testSMTLemmaSoundness(String, String)[4] | 4.002s | 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.972s | 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.957s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.924s | 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.924s | 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.940s | passed |
Standard output
938236 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 938236 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 938236 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.4ns 938252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 942114 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.86s 942130 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 942130 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 942239 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1349143876353378446.key 942239 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1349143876353378446.key 942239 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.1ns 942239 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 946148 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.91s 946164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_1349143876353378446.key 946164 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 946273 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 946273 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 946273 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 403.4ns 946273 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 950150 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 950166 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 950181 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.61ms 950291 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15408060103752691460.key 950291 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15408060103752691460.key 950291 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.8ns 950291 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 954168 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 954184 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_15408060103752691460.key 954184 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 954293 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12083568184367626168.key 954293 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12083568184367626168.key 954293 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.5ns 954293 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 958140 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.85s 958156 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_12083568184367626168.key 958156 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 958265 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_14754835407433532313.key 958265 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_14754835407433532313.key 958265 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.7ns 958265 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 962096 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.83s 962112 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_14754835407433532313.key 962112 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 962222 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10372278590069764846.key 962222 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_10372278590069764846.key 962222 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.1ns 962222 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 966006 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 966021 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_10372278590069764846.key 966021 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.6ns 966146 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4647939180340367546.key 966146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_4647939180340367546.key 966146 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.2ns 966146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 969945 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s 969961 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_4647939180340367546.key 969961 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 970070 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_16843382482026570141.key 970070 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_16843382482026570141.key 970070 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.1ns 970070 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 973885 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.81s 973901 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_16843382482026570141.key 973901 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 974010 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_9417383220962725936.key 974010 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_9417383220962725936.key 974010 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.8ns 974010 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 977810 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s 977825 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_9417383220962725936.key 977825 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 977935 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 977935 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 977935 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.1ns 977935 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 981734 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s 981750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 981750 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 981859 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_18257609643079843012.key 981859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_18257609643079843012.key 981859 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.7ns 981859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 985660 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s 985676 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_18257609643079843012.key 985676 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 985785 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_2500912794028328313.key 985785 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_2500912794028328313.key 985785 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.2ns 985785 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 989599 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.82s 989615 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_2500912794028328313.key 989615 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 989725 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_8015996047947568005.key 989725 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_8015996047947568005.key 989725 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.6ns 989725 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 993540 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.82s 993556 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_8015996047947568005.key 993572 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 993681 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11810194194567048850.key 993681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11810194194567048850.key 993681 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.4ns 993681 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 997465 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 997480 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_11810194194567048850.key 997480 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 997590 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_7693549305987716950.key 997590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_7693549305987716950.key 997590 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.5ns 997590 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1001405 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.81s 1001421 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_7693549305987716950.key 1001421 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 1001531 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6088870788317896119.key 1001531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_6088870788317896119.key 1001531 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.7ns 1001531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1005361 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.84s 1005376 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_6088870788317896119.key 1005376 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns 1005486 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_14159897864160568249.key 1005486 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_14159897864160568249.key 1005486 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.3ns 1005486 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1009301 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.82s 1009316 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_14159897864160568249.key 1009332 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.2ns 1009441 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4911597913075902539.key 1009441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4911597913075902539.key 1009441 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.2ns 1009441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1013288 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.85s 1013320 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_4911597913075902539.key 1013320 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.2ns 1013429 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_7230184963685065752.key 1013429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_7230184963685065752.key 1013429 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.1ns 1013429 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1017244 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.81s 1017260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_7230184963685065752.key 1017260 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1017369 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9376768283572492415.key 1017369 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_9376768283572492415.key 1017369 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.5ns 1017369 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1021169 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.81s 1021185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_9376768283572492415.key 1021200 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 1021310 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_2698370931017350325.key 1021310 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_2698370931017350325.key 1021310 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.8ns 1021310 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1025125 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.81s 1025140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_2698370931017350325.key 1025140 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1025250 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_8734622320329780215.key 1025250 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_8734622320329780215.key 1025250 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.9ns 1025250 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1029065 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.81s 1029080 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_8734622320329780215.key 1029080 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 1029190 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_15169709807042492109.key 1029190 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_15169709807042492109.key 1029190 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.7ns 1029190 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1033021 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.83s 1033036 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_15169709807042492109.key 1033036 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1033146 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_5266845908241108705.key 1033146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_5266845908241108705.key 1033146 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.2ns 1033146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1036976 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.83s 1036992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_5266845908241108705.key 1036992 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns