diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec index 416c5a8..e99dc6f 100644 --- a/certora/specs/StakeManager.spec +++ b/certora/specs/StakeManager.spec @@ -75,6 +75,11 @@ invariant sumOfMultipliersIsMultiplierSupply() filtered { m -> !requiresPreviousManager(m) && !requiresNextManager(m) } + { preserved with (env e){ + requireInvariant accountMPIsZeroIfBalanceIsZero(e.msg.sender); + requireInvariant accountBonusMPIsZeroIfBalanceIsZero(e.msg.sender); + } + } invariant sumOfEpochRewardsIsPendingRewards() sumOfEpochRewards == to_mathint(currentContract.pendingReward)