diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 2eb96627..7a82fca5 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -4,7 +4,6 @@ ], "solc": "solc-0.8.19", "verify": "MorphoHarness:certora/specs/ExactMath.spec", - "rule_sanity": "basic", "prover_args": [ "-depth 5", "-mediumTimeout 5", @@ -13,6 +12,7 @@ "-smt_nonLinearArithmetic true", "-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:lia2]" ], + "rule_sanity": "basic", "server": "production", "msg": "Morpho Blue Exact Math" } diff --git a/certora/confs/ExchangeRate.conf b/certora/confs/ExchangeRate.conf index 0e1f805f..5a549a5e 100644 --- a/certora/confs/ExchangeRate.conf +++ b/certora/confs/ExchangeRate.conf @@ -4,11 +4,11 @@ ], "solc": "solc-0.8.19", "verify": "MorphoHarness:certora/specs/ExchangeRate.spec", - "rule_sanity": "basic", "prover_args": [ "-smt_hashingScheme plaininjectivity", "-smt_easy_LIA true" ], + "rule_sanity": "basic", "server": "production", "msg": "Morpho Blue Exchange Rate" } diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf index 30aeeab1..0b47d05a 100644 --- a/certora/confs/Health.conf +++ b/certora/confs/Health.conf @@ -5,10 +5,10 @@ ], "solc": "solc-0.8.19", "verify": "MorphoHarness:certora/specs/Health.spec", - "rule_sanity": "basic", "prover_args": [ "-smt_hashingScheme plaininjectivity" ], + "rule_sanity": "basic", "server": "production", "msg": "Morpho Blue Health" } diff --git a/certora/confs/LibSummary.conf b/certora/confs/LibSummary.conf index dc5efc34..34526a1f 100644 --- a/certora/confs/LibSummary.conf +++ b/certora/confs/LibSummary.conf @@ -4,10 +4,10 @@ ], "solc": "solc-0.8.19", "verify": "MorphoHarness:certora/specs/LibSummary.spec", - "rule_sanity": "basic", "prover_args": [ "-smt_bitVectorTheory true" ], + "rule_sanity": "basic", "server": "production", "msg": "Morpho Blue Lib Summary" } diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf index a7a409c4..6dbec607 100644 --- a/certora/confs/Reentrancy.conf +++ b/certora/confs/Reentrancy.conf @@ -4,10 +4,10 @@ ], "solc": "solc-0.8.19", "verify": "MorphoHarness:certora/specs/Reentrancy.spec", - "rule_sanity": "basic", "prover_args": [ "-enableStorageSplitting false" ], + "rule_sanity": "basic", "server": "production", "msg": "Morpho Blue Reentrancy" } diff --git a/certora/confs/StayHealthy.conf b/certora/confs/StayHealthy.conf index 7364de17..7179c674 100644 --- a/certora/confs/StayHealthy.conf +++ b/certora/confs/StayHealthy.conf @@ -3,16 +3,13 @@ "certora/harness/MorphoHarness.sol", "src/mocks/OracleMock.sol" ], - "msg": "Morpho Blue Stay Healthy", - "process": "emv", + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/StayHealthy.spec", "prover_args": [ - "-depth 5", - "-mediumTimeout 5", - "-timeout 3600", - "-smt_hashingScheme plaininjectivity" + "-smt_hashingScheme plaininjectivity", + "-solvers [yices,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", "server": "production", - "solc": "solc-0.8.19", - "verify": "MorphoHarness:certora/specs/StayHealthy.spec" + "msg": "Morpho Blue Stay Healthy" }