This fixes some problems with the previous invariants.
The main part is adding new rules that verify that isOwner, addOwnerWithThreshold, removeOwner and swapOwner behave as intended.
In particular it checks that
getThreshold() is always between 1 and ownerCount.
isOwner returns false for SENTINEL and current contract.
isOwner's result agrees with ghostOwners.
addOwner adds an owner and doesn't change other owners.
removeOwner removes an owner and doesn't change other owners.
swapOwner removes old owner, adds new owner, and doesn't change other owners.
This fixes some problems with the previous invariants. The main part is adding new rules that verify that
isOwner
,addOwnerWithThreshold
,removeOwner
andswapOwner
behave as intended.In particular it checks that