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.417s | 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.474s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 5.449s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 5.538s | 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.528s | 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.284s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 5.541s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 5.494s | 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.336s | 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.644s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 5.775s | 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.333s | 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.504s | 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.310s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 5.291s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 5.477s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 5.382s | 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.410s | 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.695s | 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.352s | 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.519s | 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.834s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 5.400s | 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.603s | 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.480s | passed |
Standard output
1238642 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 1238642 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 1238642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.3ns 1238642 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1244237 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.59s 1244252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1244284 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.43ms 1244411 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13795551062160196203.key 1244411 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13795551062160196203.key 1244411 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.3ns 1244426 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1249695 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.27s 1249710 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_13795551062160196203.key 1249710 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 1249821 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 1249821 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 1249821 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.1ns 1249821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1255323 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.5s 1255339 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1255401 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.09ms 1255516 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15949999093956938215.key 1255516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15949999093956938215.key 1255516 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.8ns 1255516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1260737 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.22s 1260753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_15949999093956938215.key 1260753 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1260868 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_9841881486273349793.key 1260868 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_9841881486273349793.key 1260868 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.5ns 1260868 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1266247 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.38s 1266278 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_9841881486273349793.key 1266278 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1266387 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_534709017190405795.key 1266387 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_534709017190405795.key 1266387 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 201ns 1266387 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1271876 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.49s 1272097 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_534709017190405795.key 1272112 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 1272222 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_13566791759253472792.key 1272222 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_13566791759253472792.key 1272222 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.6ns 1272222 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1277493 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.27s 1277509 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_13566791759253472792.key 1277509 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ns 1277622 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_16538231850691358867.key 1277622 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_16538231850691358867.key 1277622 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.2ns 1277622 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1283081 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.46s 1283112 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_16538231850691358867.key 1283112 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1283225 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_12338728228507028186.key 1283225 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_12338728228507028186.key 1283225 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.5ns 1283225 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1288579 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.35s 1288594 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_12338728228507028186.key 1288594 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ns 1288705 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_15007312706960284507.key 1288705 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_15007312706960284507.key 1288705 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.2ns 1288705 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1293981 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s 1294012 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_15007312706960284507.key 1294012 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 1294123 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 1294123 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 1294123 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 1294123 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1299468 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.34s 1299484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1299484 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 1299602 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_1344173075829924430.key 1299602 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_1344173075829924430.key 1299602 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.9ns 1299609 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1304906 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.31s 1304937 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_1344173075829924430.key 1304937 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 1305047 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11803536675151554361.key 1305047 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11803536675151554361.key 1305047 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.6ns 1305047 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1310446 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.4s 1310477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_11803536675151554361.key 1310477 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1310586 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11224021373948035425.key 1310586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_11224021373948035425.key 1310586 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 171ns 1310586 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1315974 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.39s 1316006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_11224021373948035425.key 1316006 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.5ns 1316115 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_13282310064179697000.key 1316115 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_13282310064179697000.key 1316115 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 199ns 1316115 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1321259 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.14s 1321274 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_13282310064179697000.key 1321290 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 1321399 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9298407305796765133.key 1321399 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_9298407305796765133.key 1321399 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.6ns 1321399 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1326795 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.4s 1326811 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_9298407305796765133.key 1326826 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 1326941 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_17254166633951874348.key 1326941 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_17254166633951874348.key 1326941 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 525.6ns 1326941 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1332307 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.36s 1332323 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_17254166633951874348.key 1332323 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.1ns 1332436 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_4372692426689866517.key 1332436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_4372692426689866517.key 1332436 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.6ns 1332436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1337642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 1337658 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_4372692426689866517.key 1337658 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.7ns 1337772 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_7052518296376112695.key 1337772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_7052518296376112695.key 1337772 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.3ns 1337772 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1343276 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.5s 1343307 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_7052518296376112695.key 1343307 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 1343417 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13657438575157654579.key 1343417 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_13657438575157654579.key 1343417 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.3ns 1343417 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1348625 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 1348641 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_13657438575157654579.key 1348641 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 1348750 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5286683842555476989.key 1348750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_5286683842555476989.key 1348750 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 637.3ns 1348750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1354066 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.32s 1354113 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_5286683842555476989.key 1354129 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1354269 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_11196299607212600685.key 1354269 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_11196299607212600685.key 1354269 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 424ns 1354269 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1359440 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.17s 1359456 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_11196299607212600685.key 1359456 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.7ns 1359565 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_14383365579932889040.key 1359565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_14383365579932889040.key 1359565 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.9ns 1359565 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1364730 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s 1364746 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_14383365579932889040.key 1364746 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1364873 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_12973842674619976637.key 1364889 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_12973842674619976637.key 1364889 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.3ns 1364904 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1370197 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.31s 1370228 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_12973842674619976637.key 1370228 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.4ns 1370338 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_18075218804305658271.key 1370338 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_18075218804305658271.key 1370338 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.7ns 1370338 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1375581 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 5.25s 1375613 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_18075218804305658271.key 1375613 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns