feat: solve StayHealthy timeout

morpho-org · Oct 9, 2024 · 4446011 · 4446011
1 parent a56da03
commit 4446011
Show file tree

Hide file tree

Showing 6 changed files with 10 additions and 13 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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"
 }