From 588a4edc59820be01016c575d48e124594ca5346 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Fri, 14 Feb 2025 14:03:59 +0100 Subject: [PATCH] Update hashmap proof for CI. --- .../tests/should_succeed/hashmap/proof.json | 106 +++++++++--------- 1 file changed, 53 insertions(+), 53 deletions(-) diff --git a/creusot/tests/should_succeed/hashmap/proof.json b/creusot/tests/should_succeed/hashmap/proof.json index d726bf124..984b5c53b 100644 --- a/creusot/tests/should_succeed/hashmap/proof.json +++ b/creusot/tests/should_succeed/hashmap/proof.json @@ -37,51 +37,51 @@ "vc_add'0": { "tactic": "split_vc", "children": [ - { "prover": "cvc5@1.0.5", "time": 0.228 }, - { "prover": "cvc5@1.0.5", "time": 0.061 }, - { "prover": "cvc5@1.0.5", "time": 0.209 }, + { "prover": "cvc5@1.0.5", "time": 0.086 }, + { "prover": "cvc5@1.0.5", "time": 0.022 }, + { "prover": "cvc5@1.0.5", "time": 0.083 }, { "prover": "cvc5@1.0.5", "time": 0.157 }, { "prover": "cvc5@1.0.5", "time": 0.018 }, { "prover": "cvc5@1.0.5", "time": 0.172 }, { "prover": "cvc4@1.8", "time": 0.063 }, - { "prover": "cvc5@1.0.5", "time": 0.221 }, - { "prover": "cvc5@1.0.5", "time": 0.081 }, + { "prover": "cvc5@1.0.5", "time": 0.09 }, + { "prover": "cvc5@1.0.5", "time": 0.03 }, { "prover": "cvc4@1.8", "time": 0.07 }, { "prover": "cvc4@1.8", "time": 0.064 }, - { "prover": "cvc5@1.0.5", "time": 0.04 }, - { "prover": "cvc5@1.0.5", "time": 0.207 }, + { "prover": "cvc5@1.0.5", "time": 0.017 }, + { "prover": "cvc5@1.0.5", "time": 0.096 }, { "prover": "cvc4@1.8", "time": 0.07 }, - { "prover": "cvc4@1.8", "time": 0.11 }, - { "prover": "cvc5@1.0.5", "time": 0.086 }, - { "prover": "cvc5@1.0.5", "time": 0.092 }, + { "prover": "cvc4@1.8", "time": 0.049 }, + { "prover": "cvc5@1.0.5", "time": 0.029 }, + { "prover": "cvc5@1.0.5", "time": 0.029 }, { "prover": "cvc5@1.0.5", "time": 0.045 }, - { "prover": "cvc4@1.8", "time": 0.144 }, - { "prover": "cvc5@1.0.5", "time": 0.084 }, + { "prover": "cvc4@1.8", "time": 0.054 }, + { "prover": "cvc5@1.0.5", "time": 0.031 }, { "prover": "cvc5@1.0.5", "time": 0.053 }, - { "prover": "cvc4@1.8", "time": 0.196 }, + { "prover": "cvc4@1.8", "time": 0.076 }, { "prover": "cvc5@1.0.5", "time": 0.182 }, { "tactic": "split_vc", "children": [ { "prover": "alt-ergo@2.6.0", "time": 1.6 } ] }, { "prover": "z3@4.12.4", "time": 0.043 }, - { "prover": "cvc4@1.8", "time": 0.202 }, - { "prover": "cvc4@1.8", "time": 0.193 }, - { "prover": "cvc4@1.8", "time": 0.153 }, - { "prover": "cvc5@1.0.5", "time": 0.085 }, - { "prover": "cvc5@1.0.5", "time": 0.094 }, + { "prover": "cvc4@1.8", "time": 0.068 }, + { "prover": "cvc4@1.8", "time": 0.069 }, + { "prover": "cvc4@1.8", "time": 0.051 }, + { "prover": "cvc5@1.0.5", "time": 0.028 }, + { "prover": "cvc5@1.0.5", "time": 0.028 }, { "prover": "cvc4@1.8", "time": 0.081 }, - { "prover": "cvc4@1.8", "time": 0.144 }, - { "prover": "cvc5@1.0.5", "time": 0.087 }, - { "prover": "cvc5@1.0.5", "time": 0.032 }, - { "prover": "cvc4@1.8", "time": 0.226 }, - { "prover": "cvc4@1.8", "time": 0.16 }, + { "prover": "cvc4@1.8", "time": 0.049 }, + { "prover": "cvc5@1.0.5", "time": 0.027 }, + { "prover": "cvc5@1.0.5", "time": 0.015 }, + { "prover": "cvc4@1.8", "time": 0.078 }, + { "prover": "cvc4@1.8", "time": 0.054 }, { "prover": "cvc4@1.8", "time": 0.118 }, - { "prover": "cvc4@1.8", "time": 0.158 }, + { "prover": "cvc4@1.8", "time": 0.053 }, { "prover": "z3@4.12.4", "time": 0.034 }, - { "prover": "cvc4@1.8", "time": 0.199 }, - { "prover": "cvc4@1.8", "time": 0.145 }, - { "prover": "cvc4@1.8", "time": 0.178 }, + { "prover": "cvc4@1.8", "time": 0.069 }, + { "prover": "cvc4@1.8", "time": 0.056 }, + { "prover": "cvc4@1.8", "time": 0.064 }, { "prover": "cvc4@1.8", "time": 0.064 }, { "prover": "cvc4@1.8", "time": 0.111 }, { "prover": "cvc4@1.8", "time": 0.087 }, @@ -89,15 +89,15 @@ { "prover": "cvc5@1.0.5", "time": 0.187 }, { "prover": "cvc4@1.8", "time": 0.154 }, { "prover": "alt-ergo@2.6.0", "time": 2 }, - { "prover": "z3@4.12.4", "time": 0.049 }, + { "prover": "z3@4.12.4", "time": 0.138 }, { "prover": "cvc5@1.0.5", "time": 0.041 } ] }, - "vc_eq'0": { "prover": "cvc5@1.0.5", "time": 0.021 }, + "vc_eq'0": { "prover": "cvc5@1.0.5", "time": 0.01 }, "vc_hash'0": { "prover": "cvc5@1.0.5", "time": 0.017 }, - "vc_index_mut'0": { "prover": "cvc5@1.0.5", "time": 0.021 }, + "vc_index_mut'0": { "prover": "cvc5@1.0.5", "time": 0.01 }, "vc_len'0": { "prover": "cvc5@1.0.5", "time": 0.011 }, - "vc_v_Cons'0": { "prover": "cvc5@1.0.5", "time": 0.021 } + "vc_v_Cons'0": { "prover": "cvc5@1.0.5", "time": 0.01 } }, "M_hashmap__qyi9690720112976707081__get": { "vc_eq'0": { "prover": "cvc5@1.0.5", "time": 0.014 }, @@ -109,10 +109,10 @@ }, "M_hashmap__qyi9690720112976707081__new": { "vc_from_elem'0": { "prover": "cvc5@1.0.5", "time": 0.011 }, - "vc_new'0": { "prover": "cvc5@1.0.5", "time": 0.153 } + "vc_new'0": { "prover": "cvc5@1.0.5", "time": 0.075 } }, "M_hashmap__qyi9690720112976707081__resize": { - "vc_add'0": { "prover": "cvc5@1.0.5", "time": 0.027 }, + "vc_add'0": { "prover": "cvc5@1.0.5", "time": 0.012 }, "vc_index_mut'0": { "prover": "cvc5@1.0.5", "time": 0.017 }, "vc_len'0": { "prover": "cvc5@1.0.5", "time": 0.011 }, "vc_new'0": { "prover": "cvc5@1.0.5", "time": 0.015 }, @@ -120,16 +120,16 @@ "vc_resize'0": { "tactic": "split_vc", "children": [ - { "prover": "cvc5@1.0.5", "time": 0.183 }, + { "prover": "cvc5@1.0.5", "time": 0.079 }, { "prover": "cvc5@1.0.5", "time": 0.129 }, - { "prover": "cvc5@1.0.5", "time": 0.179 }, - { "prover": "cvc5@1.0.5", "time": 0.053 }, + { "prover": "cvc5@1.0.5", "time": 0.079 }, + { "prover": "cvc5@1.0.5", "time": 0.023 }, { "prover": "cvc5@1.0.5", "time": 0.019 }, { "prover": "cvc5@1.0.5", "time": 0.019 }, { "prover": "cvc5@1.0.5", "time": 0.185 }, - { "prover": "cvc5@1.0.5", "time": 0.069 }, - { "prover": "cvc5@1.0.5", "time": 0.067 }, - { "prover": "cvc5@1.0.5", "time": 0.074 }, + { "prover": "cvc5@1.0.5", "time": 0.023 }, + { "prover": "cvc5@1.0.5", "time": 0.025 }, + { "prover": "cvc5@1.0.5", "time": 0.025 }, { "prover": "cvc4@1.8", "time": 0.055 }, { "prover": "cvc5@1.0.5", "time": 0.173 }, { "prover": "cvc4@1.8", "time": 0.06 }, @@ -137,49 +137,49 @@ { "prover": "cvc4@1.8", "time": 0.081 }, { "prover": "cvc4@1.8", "time": 0.054 }, { "prover": "cvc4@1.8", "time": 0.064 }, - { "prover": "cvc5@1.0.5", "time": 0.073 }, - { "prover": "cvc5@1.0.5", "time": 0.08 }, + { "prover": "cvc5@1.0.5", "time": 0.023 }, + { "prover": "cvc5@1.0.5", "time": 0.028 }, { "prover": "cvc4@1.8", "time": 0.056 }, { "prover": "cvc5@1.0.5", "time": 0.022 }, { "prover": "cvc4@1.8", "time": 0.065 }, - { "prover": "cvc5@1.0.5", "time": 0.073 }, + { "prover": "cvc5@1.0.5", "time": 0.024 }, { "prover": "cvc4@1.8", "time": 0.066 }, { "prover": "cvc4@1.8", "time": 0.061 }, - { "prover": "cvc5@1.0.5", "time": 0.044 }, + { "prover": "cvc5@1.0.5", "time": 0.015 }, { "prover": "cvc5@1.0.5", "time": 0.022 }, { "prover": "cvc4@1.8", "time": 0.059 }, { "prover": "cvc4@1.8", "time": 0.057 }, { "prover": "cvc4@1.8", "time": 0.089 }, { "prover": "cvc4@1.8", "time": 0.072 }, { "prover": "cvc4@1.8", "time": 0.09 }, - { "prover": "cvc5@1.0.5", "time": 0.045 }, + { "prover": "cvc5@1.0.5", "time": 0.016 }, { "prover": "cvc4@1.8", "time": 0.073 }, { "prover": "cvc4@1.8", "time": 0.097 }, { "prover": "cvc4@1.8", "time": 0.1 }, - { "prover": "cvc5@1.0.5", "time": 0.042 }, + { "prover": "cvc5@1.0.5", "time": 0.016 }, { "prover": "cvc4@1.8", "time": 0.094 }, { "prover": "cvc4@1.8", "time": 0.103 }, { "prover": "cvc4@1.8", "time": 0.103 }, { "prover": "cvc4@1.8", "time": 0.106 }, - { "prover": "cvc4@1.8", "time": 0.085 }, + { "prover": "cvc4@1.8", "time": 0.031 }, { "prover": "z3@4.12.4", "time": 0.085 }, - { "prover": "cvc5@1.0.5", "time": 0.049 }, - { "prover": "cvc5@1.0.5", "time": 0.062 }, + { "prover": "cvc5@1.0.5", "time": 0.022 }, + { "prover": "cvc5@1.0.5", "time": 0.02 }, { "prover": "cvc5@1.0.5", "time": 0.043 }, - { "prover": "cvc5@1.0.5", "time": 0.063 }, + { "prover": "cvc5@1.0.5", "time": 0.024 }, { "prover": "cvc4@1.8", "time": 0.068 }, { "prover": "cvc4@1.8", "time": 0.068 }, - { "prover": "cvc5@1.0.5", "time": 0.051 }, + { "prover": "cvc5@1.0.5", "time": 0.023 }, { "prover": "z3@4.12.4", "time": 0.046 }, { "prover": "cvc5@1.0.5", "time": 0.029 }, { "prover": "cvc4@1.8", "time": 0.064 }, { "prover": "cvc4@1.8", "time": 0.073 }, { "prover": "cvc4@1.8", "time": 0.066 }, - { "prover": "cvc5@1.0.5", "time": 0.09 }, - { "prover": "cvc5@1.0.5", "time": 0.07 } + { "prover": "cvc5@1.0.5", "time": 0.031 }, + { "prover": "cvc5@1.0.5", "time": 0.025 } ] }, - "vc_v_Cons'0": { "prover": "cvc5@1.0.5", "time": 0.027 } + "vc_v_Cons'0": { "prover": "cvc5@1.0.5", "time": 0.012 } } } }