Revert "fix: wait for results in the CI"

This reverts commit 60991b4.
morpho-org · Nov 26, 2024 · 5179b34 · 5179b34
1 parent 60991b4
commit 5179b34
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 4 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -50,6 +50,6 @@ jobs:
           sudo mv solc-static-linux /usr/local/bin/solc-0.8.19
 
       - name: Verify ${{ matrix.conf }}
-        run: certoraRun certora/confs/${{ matrix.conf }}.conf --wait_for_results
+        run: certoraRun certora/confs/${{ matrix.conf }}.conf
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec
@@ -61,12 +61,11 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams,
     uint256 newTotalAssets = require_uint256(virtualTotalBorrowAssets(id) - repaidAssets);
 
     uint256 newBorrowerAssets = summaryMulDivUp(newBorrowerShares, newTotalAssets, newTotalShares);
-    uint256 newBorrowerAssetsDown = summaryMulDivDown(newBorrowerShares, newTotalAssets, newTotalShares);
     uint256 newBorrowerCollateral = require_uint256(borrowerCollateral - seizedAssets);
 
     assert repaidShares * borrowerCollateral >= seizedAssets * borrowerShares;
     assert borrowerShares * newBorrowerCollateral >= newBorrowerShares * borrowerCollateral;
     assert newTotalShares * virtualTotalBorrowAssets(id) >= newTotalAssets * virtualTotalBorrowShares(id);
-    require borrowerShares * virtualTotalBorrowAssets(id) * newTotalShares * newBorrowerCollateral >= newBorrowerShares * virtualTotalBorrowShares(id) * newTotalAssets * borrowerCollateral;
-    assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssetsDown * borrowerCollateral;
+    assert borrowerShares * virtualTotalBorrowAssets(id) * newTotalShares * newBorrowerCollateral >= newBorrowerShares * virtualTotalBorrowShares(id) * newTotalAssets * borrowerCollateral;
+    assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssets * borrowerCollateral;
 }