fix: repaid shares computation

morpho-org · Dec 10, 2024 · 712e6a2 · 712e6a2
1 parent ba2280f
commit 712e6a2
Showing 1 changed file with 7 additions and 2 deletions.
diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec
@@ -31,8 +31,13 @@ rule liquidateImprovePosition(env e, MorphoHarness.MarketParams marketParams, ad
     assert borrowerCollateral * collateralPrice * virtualTotalBorrowShares(id) * Util.wad() >= borrowerShares * Util.oraclePriceScale() * virtualTotalBorrowAssets(id) * lif;
 
     uint256 seizedAssets;
-    uint256 repaidShares;
-    (seizedAssets, repaidShares) = liquidate(e, marketParams, borrower, seizedAssetsInput, repaidSharesInput, data);
+    uint256 repaidAssets;
+    (seizedAssets, repaidAssets) = liquidate(e, marketParams, borrower, seizedAssetsInput, repaidSharesInput, data);
+
+    assert collateral(id, borrower) != 0;
+
+    uint256 newBorrowerShares = borrowShares(id, borrower);
+    uint256 repaidShares = assert_uint256(borrowerShares - newBorrowerShares);
 
     require !priceChanged;
     assert repaidShares * borrowerCollateral >= seizedAssets * borrowerShares;