feat: omit bad debt realization for verification

morpho-org · Feb 20, 2024 · 722b1ee · 722b1ee
1 parent 173c992
commit 722b1ee
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec
@@ -59,6 +59,8 @@ rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketP
     uint256 repaidAssets1;
     _, repaidAssets1 = liquidate(e, marketParams, borrower, seizedAssets, 0, data);
     require !priceChanged;
+    // Omit the bad debt realization case.
+    require collateral(id, borrower) != 0;
     uint256 sharesAfter = borrowShares(id, borrower);
     uint256 repaidShares1 = assert_uint256(sharesBefore - sharesAfter);