diff --git a/src/EVault/modules/Liquidation.sol b/src/EVault/modules/Liquidation.sol index 9ad9179d..e938a4e0 100644 --- a/src/EVault/modules/Liquidation.sol +++ b/src/EVault/modules/Liquidation.sol @@ -56,7 +56,6 @@ abstract contract LiquidationModule is ILiquidation, BalanceUtils, LiquidityUtil executeLiquidation(vaultCache, liqCache, minYieldBalance); } - // Munged to internal by certora to enable harnessing function calculateLiquidation( VaultCache memory vaultCache, address liquidator, @@ -158,8 +157,10 @@ abstract contract LiquidationModule is ILiquidation, BalanceUtils, LiquidityUtil uint256 maxRepayValue = liabilityValue; uint256 maxYieldValue = maxRepayValue * 1e18 / discountFactor; - // Limit yield to borrower's available collateral, and reduce repay if necessary. This can happen when borrower - // has multiple collaterals and seizing all of this one won't bring the violator back to solvency + // Limit yield to borrower's available collateral, and reduce repay if necessary. This can happen when + // seizing all of the collateral won't bring the violator back to solvency. It can happen simply because + // the account health is very low, or because borrower has multiple collaterals and liquidating this one + // is not sufficient. if (collateralValue < maxYieldValue) { maxRepayValue = collateralValue * discountFactor / 1e18; diff --git a/src/EVault/shared/Cache.sol b/src/EVault/shared/Cache.sol index f6854917..01a59f4e 100644 --- a/src/EVault/shared/Cache.sol +++ b/src/EVault/shared/Cache.sol @@ -39,7 +39,6 @@ contract Cache is Storage, Errors { // Takes a VaultCache struct, overwrites it with VaultStorage data and, if time has passed since VaultStorage // was last updated, updates VaultStorage. // Returns a boolean if the cache is different from storage. VaultCache param is updated to this block. - // Munged from private to internal by Certora to enable harnessing function initVaultCache(VaultCache memory vaultCache) internal view returns (bool dirty) { dirty = false;