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.123s | 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.033s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.220s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.107s | 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.331s | 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.252s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.317s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.194s | passed |
| [18] freshLocs.dl, \forall Heap h; \forall Object o; \forall Field f; ( elementOf(o,f,freshLocs(h))<<Trigger>> <-> o != null & !boolean::select(h,o,java.lang.Object::<created>)=TRUE ) | testSMTLemmaSoundness(String, String)[18] | 4.966s | 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.076s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.927s | 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.033s | 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.262s | 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.175s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.952s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.837s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.772s | 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.008s | 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.073s | passed |
| [4] singleton.dl, \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; ( elementOf(o,f, singleton(o2,f2))<<Trigger>> <-> o = o2 & f = f2 ) | testSMTLemmaSoundness(String, String)[4] | 5.043s | passed |
| [5] create.dl, \forall Heap h; \forall Object o; \forall Object o2; \forall Field f; any::select(create(h, o), o2, f)<<Trigger>> = \if(o = o2 & o != null & f = java.lang.Object::<created>) \then(TRUE) \else(any::select(h, o2, f)) | testSMTLemmaSoundness(String, String)[5] | 4.797s | passed |
| [6] allFields.dl, \forall Object o; \forall Field f; \forall Object o2; ( elementOf(o,f, allFields(o2))<<Trigger>> <-> o = o2 ) | testSMTLemmaSoundness(String, String)[6] | 4.793s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.952s | 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] | 4.663s | 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.006s | passed |
Standard output
1182224 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 1182224 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 1182224 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 114ns 1182226 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1187016 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.79s 1187032 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1187032 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.03ms 1187147 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1473365393612245466.key 1187147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_1473365393612245466.key 1187147 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.3ns 1187147 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1192027 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.87s 1192043 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_1473365393612245466.key 1192043 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.2ns 1192155 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 1192155 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 1192155 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.7ns 1192155 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1197029 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.88s 1197093 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1197116 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.94ms 1197228 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_2833951166319230551.key 1197228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_2833951166319230551.key 1197228 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.2ns 1197228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1202146 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 1202162 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_2833951166319230551.key 1202162 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 1202271 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8762378739901412404.key 1202271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8762378739901412404.key 1202271 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.7ns 1202271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1206927 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.66s 1206958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_8762378739901412404.key 1206958 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1207068 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_608953605466785422.key 1207068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_608953605466785422.key 1207068 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.3ns 1207068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1211732 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.67s 1211748 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_608953605466785422.key 1211748 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1211861 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6720376617191626286.key 1211861 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_6720376617191626286.key 1211861 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.4ns 1211861 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1216688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.82s 1216704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_6720376617191626286.key 1216704 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1216813 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_1193254375898112180.key 1216813 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_1193254375898112180.key 1216813 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.9ns 1216813 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1221348 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.53s 1221364 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_1193254375898112180.key 1221364 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1221476 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_10804540681478809001.key 1221476 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_10804540681478809001.key 1221476 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.7ns 1221476 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1226345 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.88s 1226376 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_10804540681478809001.key 1226376 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1226482 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6415059275385208312.key 1226482 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_6415059275385208312.key 1226482 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.2ns 1226498 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1231465 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.98s 1231497 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_6415059275385208312.key 1231497 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1231606 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 1231606 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 1231606 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.1ns 1231606 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1236498 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 1236514 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1236529 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 1236639 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_16125581386979482736.key 1236639 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_16125581386979482736.key 1236639 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.1ns 1236639 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1241734 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.09s 1241750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_16125581386979482736.key 1241750 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 1241859 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8574957842508071138.key 1241859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8574957842508071138.key 1241859 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.8ns 1241859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1246841 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.97s 1246856 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_8574957842508071138.key 1246856 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1246966 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_7321179426409656201.key 1246966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_7321179426409656201.key 1246966 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 430.7ns 1246966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1252173 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 1252189 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_7321179426409656201.key 1252189 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.3ns 1252297 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12880304267331810281.key 1252297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12880304267331810281.key 1252297 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.2ns 1252297 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1257410 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s 1257441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_12880304267331810281.key 1257441 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 1257550 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_3049153477466543649.key 1257550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_3049153477466543649.key 1257550 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 367ns 1257550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1262739 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.18s 1262755 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_3049153477466543649.key 1262755 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1262868 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_1410782596576182701.key 1262868 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_1410782596576182701.key 1262868 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.1ns 1262868 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1267936 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.06s 1267952 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_1410782596576182701.key 1267952 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 1268063 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_17390638117912933283.key 1268063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_17390638117912933283.key 1268063 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.6ns 1268063 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1272889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.83s 1272920 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_17390638117912933283.key 1272920 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.1ns 1273061 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15731448711736150238.key 1273061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15731448711736150238.key 1273061 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.9ns 1273061 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1277972 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 1277987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_15731448711736150238.key 1277987 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1278106 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14732121754615746633.key 1278106 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14732121754615746633.key 1278106 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 563.6ns 1278106 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1283014 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.9s 1283029 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_14732121754615746633.key 1283029 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1283139 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_15342905963321900008.key 1283139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_15342905963321900008.key 1283139 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.2ns 1283139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1288270 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s 1288286 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_15342905963321900008.key 1288286 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.7ns 1288401 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_15769545276172342337.key 1288401 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_15769545276172342337.key 1288401 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.1ns 1288401 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1293435 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.04s 1293466 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_15769545276172342337.key 1293466 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ns 1293576 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_16512512048588777220.key 1293576 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_16512512048588777220.key 1293576 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.5ns 1293576 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1298389 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.81s 1298420 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_16512512048588777220.key 1298420 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.8ns 1298529 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_8584679589946189706.key 1298529 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_8584679589946189706.key 1298529 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.4ns 1298529 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1303237 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.7s 1303253 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_8584679589946189706.key 1303253 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1303367 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6244716839132885982.key 1303367 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_6244716839132885982.key 1303367 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.2ns 1303367 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1307999 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.64s 1308030 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_6244716839132885982.key 1308030 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.2ns