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.231s | 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.313s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.214s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.284s | 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.337s | 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.243s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.265s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.347s | 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.403s | 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.297s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.346s | 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.313s | 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.331s | 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.350s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.377s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.346s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.373s | 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.340s | 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.343s | 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.301s | 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.265s | 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.294s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.283s | 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.235s | 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.208s | passed |
Standard output
961202 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 961202 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 961202 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 961218 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 965406 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.2s 965422 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 965422 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 965547 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_9984980735381615708.key 965547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_9984980735381615708.key 965547 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.8ns 965547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 969762 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.21s 969778 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_9984980735381615708.key 969778 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 969887 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 969887 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 969887 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.7ns 969887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 974084 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.2s 974100 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 974115 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.88ms 974230 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3401330634398233704.key 974230 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_3401330634398233704.key 974230 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.7ns 974230 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 978406 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 978422 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_3401330634398233704.key 978422 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 978531 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_6405487535116375476.key 978531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_6405487535116375476.key 978531 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.3ns 978531 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 982664 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 982679 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_6405487535116375476.key 982679 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 982796 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_17692790990840022676.key 982796 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_17692790990840022676.key 982796 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.5ns 982796 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 986965 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 986980 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_17692790990840022676.key 986980 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 987090 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8835713021610614842.key 987090 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_8835713021610614842.key 987090 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 256ns 987090 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 991244 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.15s 991260 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_8835713021610614842.key 991260 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.4ns 991373 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_16204287050372705756.key 991373 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_16204287050372705756.key 991373 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.5ns 991373 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 995477 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.11s 995493 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_16204287050372705756.key 995493 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.1ns 995608 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_4771926233147934810.key 995608 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_4771926233147934810.key 995608 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.8ns 995608 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 999686 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 999702 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_4771926233147934810.key 999702 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 999816 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_14259219081185684501.key 999816 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_14259219081185684501.key 999816 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.8ns 999816 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1003906 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 1003921 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_14259219081185684501.key 1003921 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 1004047 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 1004047 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 1004047 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.9ns 1004047 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1008219 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 1008235 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1008235 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 885ns 1008360 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11599895631010393224.key 1008360 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_11599895631010393224.key 1008360 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.7ns 1008360 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1012446 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s 1012462 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_11599895631010393224.key 1012462 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 1012575 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_14086412287609869973.key 1012575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_14086412287609869973.key 1012575 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.8ns 1012575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1016734 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.15s 1016749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_14086412287609869973.key 1016749 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1016859 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_5032422470176541880.key 1016859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_5032422470176541880.key 1016859 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.5ns 1016859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1021055 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.2s 1021086 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_5032422470176541880.key 1021086 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 1021196 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_4356646437786537773.key 1021196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_4356646437786537773.key 1021196 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.7ns 1021196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1025313 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.12s 1025328 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_4356646437786537773.key 1025328 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1025439 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13793159707515850763.key 1025439 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_13793159707515850763.key 1025439 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 253ns 1025439 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1029573 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 1029589 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_13793159707515850763.key 1029589 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1029705 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2830675025463288246.key 1029705 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_2830675025463288246.key 1029705 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 265ns 1029705 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1033919 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 1033934 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_2830675025463288246.key 1033934 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1034052 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18044541940429340028.key 1034052 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_18044541940429340028.key 1034052 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.4ns 1034052 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1038326 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 1038342 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_18044541940429340028.key 1038342 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1038455 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15834015262239549717.key 1038455 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_15834015262239549717.key 1038455 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.7ns 1038455 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1042628 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 1042643 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_15834015262239549717.key 1042643 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12ns 1042753 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11521793827993634949.key 1042753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11521793827993634949.key 1042753 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.1ns 1042753 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1046939 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s 1046955 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_11521793827993634949.key 1046955 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 1047066 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7780763104625221283.key 1047066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_7780763104625221283.key 1047066 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.4ns 1047066 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1051257 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.2s 1051288 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_7780763104625221283.key 1051288 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 1051397 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_8423397898495093150.key 1051397 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_8423397898495093150.key 1051397 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.5ns 1051397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1055618 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 1055633 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_8423397898495093150.key 1055633 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1055747 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6363876072307508637.key 1055747 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_6363876072307508637.key 1055747 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.1ns 1055747 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1059999 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1060014 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_6363876072307508637.key 1060014 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 1060124 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_9505652891495821588.key 1060124 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_9505652891495821588.key 1060124 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.2ns 1060124 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1064331 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 1064362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_9505652891495821588.key 1064362 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1064471 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_5392223522724023825.key 1064471 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_5392223522724023825.key 1064471 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.1ns 1064471 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1068717 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.25s 1068732 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_5392223522724023825.key 1068732 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.9ns