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.669s | 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.742s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.630s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.753s | 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] | 6.499s | 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.477s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.368s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.453s | 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.493s | 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.465s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.724s | 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.423s | 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.537s | 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.437s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.394s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.434s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.436s | 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.724s | 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.644s | 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.597s | 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.685s | 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.792s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.681s | 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.677s | 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.663s | passed |
Standard output
1285700 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 1285700 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 1285700 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.8ns 1285715 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1291287 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.57s 1291303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1291318 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.76ms 1291428 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_16566022112002947353.key 1291428 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_16566022112002947353.key 1291428 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.7ns 1291428 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1297021 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.59s 1297037 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_16566022112002947353.key 1297037 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ns 1297153 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 1297153 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 1297153 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.2ns 1297153 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1302645 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.48s 1302661 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1302676 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.11ms 1302797 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_4837072419577655096.key 1302797 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_4837072419577655096.key 1302797 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.4ns 1302797 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1308253 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.46s 1308284 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_4837072419577655096.key 1308284 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 1308394 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_4886055780746580447.key 1308394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_4886055780746580447.key 1308394 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.5ns 1308394 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1313934 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.54s 1313970 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_4886055780746580447.key 1313970 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.3ns 1314079 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_9868505288300357681.key 1314079 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_9868505288300357681.key 1314079 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 299ns 1314079 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1319745 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.66s 1319761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_9868505288300357681.key 1319761 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ns 1319871 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_12805901027240846142.key 1319871 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_12805901027240846142.key 1319871 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.6ns 1319871 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1325412 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.53s 1325443 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_12805901027240846142.key 1325443 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 1325552 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3387748952089155757.key 1325552 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_3387748952089155757.key 1325552 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 434.8ns 1325552 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1331100 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.54s 1331115 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_3387748952089155757.key 1331115 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.1ns 1331229 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_2305342572519885347.key 1331229 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_2305342572519885347.key 1331229 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.5ns 1331229 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1336746 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.52s 1336782 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_2305342572519885347.key 1336782 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ns 1336892 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5378764687382220133.key 1336892 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5378764687382220133.key 1336892 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.9ns 1336892 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1342420 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.53s 1342436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5378764687382220133.key 1342452 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 1342561 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 1342561 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 1342561 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.6ns 1342561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1348162 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.6s 1348178 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1348193 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 1348303 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_4393012582338920270.key 1348303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_4393012582338920270.key 1348303 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 442.1ns 1348303 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1353805 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.5s 1353821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_4393012582338920270.key 1353821 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 1353933 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8647035159233158216.key 1353933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8647035159233158216.key 1353933 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.5ns 1353933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1359546 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.61s 1359561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_8647035159233158216.key 1359561 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 1359686 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_2263882640068618784.key 1359686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_2263882640068618784.key 1359686 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 449.4ns 1359686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1366047 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.37s 1366078 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_2263882640068618784.key 1366078 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 1366186 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12077883324393854243.key 1366186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_12077883324393854243.key 1366186 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 460.6ns 1366186 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1371535 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.35s 1371551 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_12077883324393854243.key 1371551 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ns 1371663 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_5751896193060185405.key 1371663 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_5751896193060185405.key 1371663 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.4ns 1371663 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1376891 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.23s 1376922 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_5751896193060185405.key 1376922 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 1377032 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_14613555644700957933.key 1377032 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_14613555644700957933.key 1377032 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 284ns 1377032 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1382345 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.31s 1382360 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_14613555644700957933.key 1382360 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ns 1382485 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_518992518523200749.key 1382485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_518992518523200749.key 1382485 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.9ns 1382485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1387837 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.35s 1387868 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_518992518523200749.key 1387868 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 1387978 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_11831639586434888223.key 1387978 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_11831639586434888223.key 1387978 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 264ns 1387978 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1393315 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.33s 1393330 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_11831639586434888223.key 1393330 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 1393443 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_1704903302915023630.key 1393443 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_1704903302915023630.key 1393443 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.7ns 1393443 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1398742 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.29s 1398758 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_1704903302915023630.key 1398758 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ns 1398867 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_2123214992874525801.key 1398867 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_2123214992874525801.key 1398867 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.7ns 1398867 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1404264 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.4s 1404280 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_2123214992874525801.key 1404296 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.1ns 1404405 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_13602969999469981798.key 1404405 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_13602969999469981798.key 1404405 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.3ns 1404405 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1409702 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.3s 1409718 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_13602969999469981798.key 1409733 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ns 1409843 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3638025398135877918.key 1409843 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3638025398135877918.key 1409843 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 474.3ns 1409843 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1415098 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.25s 1415113 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_3638025398135877918.key 1415129 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 1415238 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_16281576005790688544.key 1415238 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_16281576005790688544.key 1415238 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.1ns 1415238 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1420532 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.29s 1420548 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_16281576005790688544.key 1420563 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ns 1420673 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_690670250744371374.key 1420673 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_690670250744371374.key 1420673 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.4ns 1420673 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1425979 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.3s 1425994 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_690670250744371374.key 1425994 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns