mirror of https://github.com/logos-co/staking.git
chore(StakeManager.spec): fix wrong Sload requirement
This commit is contained in:
parent
fefc4dc4f0
commit
e2646f8e1b
|
@ -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()
|
||||
|
|
Loading…
Reference in New Issue