From fc3578ee48c189f31d46ade3bf6f7b9315ff90fd Mon Sep 17 00:00:00 2001 From: Ricardo Guilherme Schmidt <3esmit@gmail.com> Date: Thu, 3 Oct 2024 00:24:12 -0300 Subject: [PATCH] chore(StakeManager.spec): fix wrong Sload requirement --- certora/specs/StakeManager.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec index 350ac9f..416c5a8 100644 --- a/certora/specs/StakeManager.spec +++ b/certora/specs/StakeManager.spec @@ -61,7 +61,7 @@ hook Sstore accounts[KEY address addr].totalMP uint256 newValue (uint256 oldValu } hook Sload uint256 newValue accounts[KEY address addr].totalMP { - require sumOfBalances >= to_mathint(newValue); + require sumOfMultipliers >= to_mathint(newValue); } invariant sumOfBalancesIsTotalSupplyBalance()