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] | 4.066s | 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] | 4.097s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.049s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.064s | 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] | 4.065s | 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] | 4.095s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.065s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.065s | 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.050s | 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] | 4.080s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.206s | 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] | 4.066s | passed |
| [21] store.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; \forall any v; any::select(store(h,o,f,v), o2, f2)<<Trigger>> = \if(o = o2 & f = f2 & f != java.lang.Object::<created>) \then(v) \else(any::select(h, o2, f2)) | testSMTLemmaSoundness(String, String)[21] | 4.049s | 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] | 4.065s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.081s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.095s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.081s | 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.159s | 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.175s | 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.142s | 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.113s | 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.078s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.071s | 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.066s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 4.050s | passed |
Standard output
958311 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 958311 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 958311 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.5ns 958311 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 962375 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.06s 962391 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 962406 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.49ms 962516 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13031172552347450342.key 962516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_13031172552347450342.key 962516 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 297.4ns 962516 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 966550 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.03s 966566 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_13031172552347450342.key 966566 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ns 966675 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 966675 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 966675 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.8ns 966675 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 970693 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.02s 970709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 970740 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.41ms 970850 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_17505569015015030062.key 970850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_17505569015015030062.key 970850 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.3ns 970850 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 974852 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.01s 974867 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_17505569015015030062.key 974883 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.7ns 974992 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_3093668444250770043.key 974992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_3093668444250770043.key 974992 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.7ns 974992 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 978964 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.98s 978980 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_3093668444250770043.key 978995 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.2ns 979105 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_2120408502140277830.key 979105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_2120408502140277830.key 979105 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 457.1ns 979105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 983059 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.95s 983075 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_2120408502140277830.key 983075 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 983184 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17784688931293310695.key 983184 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_17784688931293310695.key 983184 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.9ns 983184 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 987124 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s 987140 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_17784688931293310695.key 987140 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.2ns 987255 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_17026104730683378092.key 987255 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_17026104730683378092.key 987255 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.8ns 987255 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 991180 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s 991196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_17026104730683378092.key 991196 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 991321 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_2512629131546237516.key 991321 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_2512629131546237516.key 991321 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.9ns 991321 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 995246 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 995261 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_2512629131546237516.key 995261 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 995371 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5572035627650018717.key 995371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_5572035627650018717.key 995371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270ns 995371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 999312 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s 999327 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_5572035627650018717.key 999327 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 999437 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 999437 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 999437 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.8ns 999437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1003409 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.97s 1003424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1003424 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 1003534 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_9009172392060507805.key 1003534 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_9009172392060507805.key 1003534 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 436ns 1003534 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1007442 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.91s 1007458 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_9009172392060507805.key 1007473 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 1007583 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_2898260677602827966.key 1007583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_2898260677602827966.key 1007583 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.7ns 1007583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1011522 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s 1011538 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_2898260677602827966.key 1011538 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1011647 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_5825565273806036954.key 1011647 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_5825565273806036954.key 1011647 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.4ns 1011647 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1015571 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s 1015587 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_5825565273806036954.key 1015587 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.7ns 1015712 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_504427493343400811.key 1015712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_504427493343400811.key 1015712 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 260ns 1015712 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1019667 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.96s 1019698 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_504427493343400811.key 1019698 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1019807 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_18401567685812529963.key 1019807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_18401567685812529963.key 1019807 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.7ns 1019807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1023748 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s 1023764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_18401567685812529963.key 1023764 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 1023873 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_3794856315673314442.key 1023873 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_3794856315673314442.key 1023873 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268ns 1023873 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1027812 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s 1027828 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_3794856315673314442.key 1027828 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 1027938 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15999912608449374134.key 1027938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_15999912608449374134.key 1027938 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 278.3ns 1027938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1031863 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 1031878 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_15999912608449374134.key 1031878 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.4ns 1031988 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_17897729053709349423.key 1031988 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_17897729053709349423.key 1031988 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.5ns 1031988 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1035943 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.95s 1035958 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_17897729053709349423.key 1035958 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 1036068 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_15552220832128580116.key 1036068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_15552220832128580116.key 1036068 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.5ns 1036068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1039993 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s 1040024 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_15552220832128580116.key 1040024 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ns 1040134 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_2459200624524214817.key 1040134 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_2459200624524214817.key 1040134 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.6ns 1040134 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1044058 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 1044074 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_2459200624524214817.key 1044074 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1044183 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_2630817860753372273.key 1044183 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_2630817860753372273.key 1044183 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.9ns 1044183 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1048123 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s 1048139 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_2630817860753372273.key 1048139 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 1048248 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_8433799938304220608.key 1048248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_8433799938304220608.key 1048248 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.2ns 1048248 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1052204 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.96s 1052219 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_8433799938304220608.key 1052219 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1052329 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_10141718927473719903.key 1052329 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_10141718927473719903.key 1052329 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 457.7ns 1052329 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1056299 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.97s 1056315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_10141718927473719903.key 1056315 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.8ns 1056424 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_8729626739342329738.key 1056424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_8729626739342329738.key 1056424 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.7ns 1056424 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1060364 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s 1060379 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_8729626739342329738.key 1060395 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.5ns