From 1c584ef470d520de4d3c061935fe7ab6bacdc8a0 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 10 Dec 2024 16:00:47 +0100 Subject: [PATCH] refactor: repayableShares as uint256 --- certora/specs/Reverts.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec index 1e5a4f0..e60e059 100644 --- a/certora/specs/Reverts.spec +++ b/certora/specs/Reverts.spec @@ -107,7 +107,7 @@ rule excessivePreliquidationWithAssetsReverts(env e, address borrower, uint256 s currentContract.PRE_LCF_1, currentContract.PRE_LCF_2) ; - mathint repayableShares = summaryWMulDown(MORPHO.borrowShares(currentContract.ID, borrower), preLCF); + uint256 repayableShares = summaryWMulDown(MORPHO.borrowShares(currentContract.ID, borrower), preLCF); preLiquidate@withrevert(e, borrower, seizedAssets, 0, data); @@ -138,7 +138,7 @@ rule excessivePreliquidationWithSharesReverts(env e, address borrower, uint256 r currentContract.PRE_LCF_1, currentContract.PRE_LCF_2); - mathint repayableShares = summaryWMulDown(borrowerShares, preLCF); + uint256 repayableShares = summaryWMulDown(borrowerShares, preLCF); preLiquidate@withrevert(e, borrower, 0, repaidShares, data);