diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index b37ba6e22..69d1fd85e 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -21,8 +21,8 @@ methods { */ //invariant voteStartBeforeVoteEnd1(uint256 pId) proposalSnapshot(pId) < proposalDeadline(pId) invariant voteStartBeforeVoteEnd(uint256 pId) - (proposalSnapshot(pId) == 0 <=> proposalDeadline(pId) == 0) && - proposalSnapshot(pId) < proposalDeadline(pId) + (proposalSnapshot(pId) > 0 => proposalSnapshot(pId) < proposalDeadline(pId)) + && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0) /** * A proposal cannot be both executed and canceled.