From 47aaecf4185787dc589a85157ff9f651f3985da7 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 20 Dec 2023 10:03:31 +0100 Subject: [PATCH] fix: depth 3 for AccrueInterest --- certora/confs/AccrueInterest.conf | 2 ++ certora/confs/AssetsAccounting.conf | 1 + certora/confs/ConsistentState.conf | 1 + certora/confs/ExactMath.conf | 1 + certora/confs/Health.conf | 1 + certora/confs/LibSummary.conf | 1 + certora/confs/Liveness.conf | 1 + certora/confs/RatioMath.conf | 1 + certora/confs/Reentrancy.conf | 1 + certora/confs/Reverts.conf | 1 + certora/confs/Transfer.conf | 1 + 11 files changed, 12 insertions(+) diff --git a/certora/confs/AccrueInterest.conf b/certora/confs/AccrueInterest.conf index a923c628e..8f8c26d72 100644 --- a/certora/confs/AccrueInterest.conf +++ b/certora/confs/AccrueInterest.conf @@ -4,9 +4,11 @@ ], "verify": "MorphoHarness:certora/specs/AccrueInterest.spec", "prover_args": [ + "-depth 3", "-smt_hashingScheme plaininjectivity", "-mediumTimeout 30" ], "rule_sanity": "basic", + "server": "production", "msg": "Morpho Blue Accrue Interest" } diff --git a/certora/confs/AssetsAccounting.conf b/certora/confs/AssetsAccounting.conf index 8bdc141ec..6dcd57dc6 100644 --- a/certora/confs/AssetsAccounting.conf +++ b/certora/confs/AssetsAccounting.conf @@ -4,5 +4,6 @@ ], "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec", "rule_sanity": "basic", + "server": "production", "msg": "Morpho Blue Assets Accounting" } diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf index 9691cfcb1..fdfa6e17a 100644 --- a/certora/confs/ConsistentState.conf +++ b/certora/confs/ConsistentState.conf @@ -4,5 +4,6 @@ ], "verify": "MorphoHarness:certora/specs/ConsistentState.spec", "rule_sanity": "basic", + "server": "production", "msg": "Morpho Blue Consistent State" } diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 26a0d6d2b..947e98bb4 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -8,5 +8,6 @@ "-smt_hashingScheme plaininjectivity", "-mediumTimeout 30" ], + "server": "production", "msg": "Morpho Blue Exact Math" } diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf index a75fa1bb6..f361bf43d 100644 --- a/certora/confs/Health.conf +++ b/certora/confs/Health.conf @@ -8,5 +8,6 @@ "prover_args": [ "-smt_hashingScheme plaininjectivity" ], + "server": "production", "msg": "Morpho Blue Health" } diff --git a/certora/confs/LibSummary.conf b/certora/confs/LibSummary.conf index 4aebed846..f931810eb 100644 --- a/certora/confs/LibSummary.conf +++ b/certora/confs/LibSummary.conf @@ -4,5 +4,6 @@ ], "verify": "MorphoHarness:certora/specs/LibSummary.spec", "rule_sanity": "basic", + "server": "production", "msg": "Morpho Blue Lib Summary" } diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf index 2659b17b1..211a0897a 100644 --- a/certora/confs/Liveness.conf +++ b/certora/confs/Liveness.conf @@ -4,5 +4,6 @@ ], "verify": "MorphoInternalAccess:certora/specs/Liveness.spec", "rule_sanity": "basic", + "server": "production", "msg": "Morpho Blue Liveness" } diff --git a/certora/confs/RatioMath.conf b/certora/confs/RatioMath.conf index 700c436e2..9062f1b14 100644 --- a/certora/confs/RatioMath.conf +++ b/certora/confs/RatioMath.conf @@ -9,5 +9,6 @@ "-mediumTimeout 30", "-timeout 3600" ], + "server": "production", "msg": "Morpho Blue Ratio Math" } diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf index 0fe902cfb..84019dceb 100644 --- a/certora/confs/Reentrancy.conf +++ b/certora/confs/Reentrancy.conf @@ -7,5 +7,6 @@ "prover_args": [ "-enableStorageSplitting false" ], + "server": "production", "msg": "Morpho Blue Reentrancy" } diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf index 92ce70bff..6992b6b4b 100644 --- a/certora/confs/Reverts.conf +++ b/certora/confs/Reverts.conf @@ -4,5 +4,6 @@ ], "verify": "MorphoHarness:certora/specs/Reverts.spec", "rule_sanity": "basic", + "server": "production", "msg": "Morpho Blue Reverts" } diff --git a/certora/confs/Transfer.conf b/certora/confs/Transfer.conf index ac1bdeee1..6425f56a5 100644 --- a/certora/confs/Transfer.conf +++ b/certora/confs/Transfer.conf @@ -7,5 +7,6 @@ ], "verify": "TransferHarness:certora/specs/Transfer.spec", "rule_sanity": "basic", + "server": "production", "msg": "Morpho Blue Transfer" }