From 47d75580a24a0382fb7c90c6b077ab1cb443cb9e Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Thu, 12 Dec 2024 15:44:37 +0100
Subject: [PATCH] chore: one assert

---
 certora/specs/LiquidateBuffer.spec | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec
index f07d305f..be4d42b9 100644
--- a/certora/specs/LiquidateBuffer.spec
+++ b/certora/specs/LiquidateBuffer.spec
@@ -34,12 +34,11 @@ rule liquidateImprovePosition(env e, MorphoHarness.MarketParams marketParams, ad
     uint256 repaidAssets;
     (seizedAssets, repaidAssets) = liquidate(e, marketParams, borrower, seizedAssetsInput, repaidSharesInput, data);
 
-
     uint256 newBorrowerShares = borrowShares(id, borrower);
     uint256 repaidShares = assert_uint256(borrowerShares - newBorrowerShares);
 
     require !priceChanged;
-    assert collateral(id, borrower) != 0;
+    require collateral(id, borrower) != 0;
     assert repaidShares * borrowerCollateral >= seizedAssets * borrowerShares;
     // assert borrowerShares * newBorrowerCollateral >= newBorrowerShares * borrowerCollateral;
     // assert newTotalShares * OldVirtualTotalBorrowAssets >= newTotalAssets * OldVirtualTotalBorrowShares;