chore: try out multiple seeds for Z3

morpho-org · Nov 30, 2024 · 18c6243 · 18c6243
1 parent 5179b34
commit 18c6243
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 1 deletion.
diff --git a/certora/confs/LiquidateBuffer.conf b/certora/confs/LiquidateBuffer.conf
@@ -5,6 +5,14 @@
   ],
   "solc": "solc-0.8.19",
   "verify": "MorphoLiquidateHarness:certora/specs/LiquidateBuffer.spec",
+  "prover_args": [
+    "-depth 5",
+    "-mediumTimeout 5",
+    "-timeout 3600",
+    "-adaptiveSolverConfig false",
+    "-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 Liquidate Buffer"

diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec
@@ -67,5 +67,5 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams,
     assert borrowerShares * newBorrowerCollateral >= newBorrowerShares * borrowerCollateral;
     assert newTotalShares * virtualTotalBorrowAssets(id) >= newTotalAssets * virtualTotalBorrowShares(id);
     assert borrowerShares * virtualTotalBorrowAssets(id) * newTotalShares * newBorrowerCollateral >= newBorrowerShares * virtualTotalBorrowShares(id) * newTotalAssets * borrowerCollateral;
-    assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssets * borrowerCollateral;
+    // assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssetsDown * borrowerCollateral;
 }