From 5a71e1089cb730b6fbb28b5744925e8725ab5df2 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 29 Jan 2025 13:44:19 +0100 Subject: [PATCH 1/4] chore: disable cache --- certora/confs/StayHealthy.conf | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/confs/StayHealthy.conf b/certora/confs/StayHealthy.conf index 05d82fa3..41afa884 100644 --- a/certora/confs/StayHealthy.conf +++ b/certora/confs/StayHealthy.conf @@ -7,6 +7,7 @@ "solc": "solc-0.8.19", "verify": "MorphoHarness:certora/specs/StayHealthy.spec", "prover_args": [ + "-cache none", "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" ], "rule_sanity": "basic", From 4e67d2fe0c3dd98acc88e1facdf2f08d3198b29b Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 29 Jan 2025 16:25:16 +0100 Subject: [PATCH 2/4] fix: certora cache instead of ATP cache --- certora/confs/StayHealthy.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/confs/StayHealthy.conf b/certora/confs/StayHealthy.conf index 41afa884..bbe0bfd5 100644 --- a/certora/confs/StayHealthy.conf +++ b/certora/confs/StayHealthy.conf @@ -7,9 +7,9 @@ "solc": "solc-0.8.19", "verify": "MorphoHarness:certora/specs/StayHealthy.spec", "prover_args": [ - "-cache none", "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" ], + "cache": "none", "rule_sanity": "basic", "server": "production", "msg": "Morpho Blue Stay Healthy" From b9eb97fc2586ad57bec9db4d1e432efb53504303 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 29 Jan 2025 17:29:54 +0100 Subject: [PATCH 3/4] feat: multi assert check --- certora/confs/StayHealthy.conf | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/confs/StayHealthy.conf b/certora/confs/StayHealthy.conf index bbe0bfd5..18647aee 100644 --- a/certora/confs/StayHealthy.conf +++ b/certora/confs/StayHealthy.conf @@ -10,6 +10,7 @@ "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" ], "cache": "none", + "multi_assert_check": true, "rule_sanity": "basic", "server": "production", "msg": "Morpho Blue Stay Healthy" From 80f5a53685c4aace6243dd6f98ae2212b08f586f Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 29 Jan 2025 17:45:34 +0100 Subject: [PATCH 4/4] chore: remove cache none --- certora/confs/StayHealthy.conf | 1 - 1 file changed, 1 deletion(-) diff --git a/certora/confs/StayHealthy.conf b/certora/confs/StayHealthy.conf index 18647aee..c851df37 100644 --- a/certora/confs/StayHealthy.conf +++ b/certora/confs/StayHealthy.conf @@ -9,7 +9,6 @@ "prover_args": [ "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" ], - "cache": "none", "multi_assert_check": true, "rule_sanity": "basic", "server": "production",