From ac729e0ecf8006dd8b0c0a28cdf4d89965918be5 Mon Sep 17 00:00:00 2001
From: Shelly Grossman <shelly@certora.com>
Date: Mon, 8 Nov 2021 14:57:51 +0200
Subject: [PATCH] fix simple vote end before start

---
 certora/specs/GovernorBase.spec | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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.