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] | 2.507s | 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] | 2.509s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 2.501s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 2.500s | 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] | 2.507s | 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] | 2.508s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 2.514s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 2.544s | 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] | 2.513s | 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] | 2.550s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 2.610s | 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] | 2.512s | 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] | 2.516s | 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] | 2.518s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 2.501s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 2.504s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 2.512s | 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] | 2.611s | 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] | 2.612s | 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] | 2.570s | 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] | 2.608s | 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] | 2.549s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 2.527s | 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] | 2.528s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 2.508s | passed |
Standard output
587535 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 587536 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 587536 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 587539 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 590019 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 590019 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 590035 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.09ms 590144 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_11411981971671655180.key 590144 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_11411981971671655180.key 590144 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.2ns 590144 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 592621 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 592621 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_11411981971671655180.key 592621 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ns 592746 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 592746 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 592746 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.8ns 592746 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 595202 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 595218 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 595249 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.89ms 595359 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15772268024483550594.key 595359 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_15772268024483550594.key 595359 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.3ns 595359 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 597801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 597817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_15772268024483550594.key 597817 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 597929 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12885532924181499623.key 597929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_12885532924181499623.key 597929 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.3ns 597929 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 600423 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 600423 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_12885532924181499623.key 600423 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 600538 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_17306671700294838667.key 600538 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_17306671700294838667.key 600538 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.9ns 600538 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 602962 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 602978 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_17306671700294838667.key 602978 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 603087 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2324863351658133022.key 603087 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_2324863351658133022.key 603087 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 267ns 603087 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 605490 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 605506 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_2324863351658133022.key 605506 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ns 605615 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13315529089709028681.key 605615 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13315529089709028681.key 605615 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.6ns 605615 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 608015 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 608030 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_13315529089709028681.key 608030 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ns 608143 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_2989509045849910622.key 608143 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_2989509045849910622.key 608143 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.8ns 608143 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 610524 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 610540 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_2989509045849910622.key 610540 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 610651 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_965903639297521985.key 610651 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_965903639297521985.key 610651 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.8ns 610651 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 613044 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 613044 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_965903639297521985.key 613044 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ns 613159 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 613159 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 613159 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.7ns 613159 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 615540 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 615556 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 615556 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 615669 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15622857837738159013.key 615669 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15622857837738159013.key 615669 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.4ns 615669 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 618043 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 618058 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_15622857837738159013.key 618058 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ns 618170 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8254249674253875373.key 618170 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8254249674253875373.key 618170 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.4ns 618170 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 620546 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 620561 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_8254249674253875373.key 620561 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ns 620671 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9530135473180774613.key 620671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_9530135473180774613.key 620671 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.2ns 620671 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 623053 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 623068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_9530135473180774613.key 623068 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 623178 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11923522040236149443.key 623178 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_11923522040236149443.key 623178 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.5ns 623178 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 625561 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 625576 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_11923522040236149443.key 625576 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 625686 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_3056756085299675468.key 625686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_3056756085299675468.key 625686 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.8ns 625686 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 628075 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 628075 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_3056756085299675468.key 628075 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 628200 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_13930703777267636833.key 628200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_13930703777267636833.key 628200 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.7ns 628200 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 630619 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 630619 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_13930703777267636833.key 630635 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 630744 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_11753812548098117454.key 630744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_11753812548098117454.key 630744 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 276ns 630744 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 633142 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 633142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_11753812548098117454.key 633142 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 633258 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_1097591668071632488.key 633258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_1097591668071632488.key 633258 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.3ns 633258 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 635684 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 635700 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_1097591668071632488.key 635700 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 635809 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_5418612361257095074.key 635809 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_5418612361257095074.key 635809 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.7ns 635809 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 638196 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 638211 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_5418612361257095074.key 638211 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 638321 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_10288144365710658300.key 638321 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_10288144365710658300.key 638321 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.6ns 638321 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 640708 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 640708 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_10288144365710658300.key 640723 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 640837 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_5302331738346004880.key 640837 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_5302331738346004880.key 640837 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 273ns 640837 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 643231 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 643246 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_5302331738346004880.key 643246 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ns 643356 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_263892583222507573.key 643356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_263892583222507573.key 643356 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 185ns 643356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 645742 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 645742 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_263892583222507573.key 645742 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 645858 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_11878059503198894914.key 645858 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_11878059503198894914.key 645858 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.1ns 645858 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 648237 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 648252 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_11878059503198894914.key 648252 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 648362 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_9807606643164400708.key 648362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_9807606643164400708.key 648362 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.4ns 648362 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 650749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 650764 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_9807606643164400708.key 650764 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns