From ddaf4bccf2c195e8d4cb6b9f6943f2df08ffc54d Mon Sep 17 00:00:00 2001
From: Hadrien Croubois <hadrien.croubois@gmail.com>
Date: Thu, 16 Mar 2023 20:56:33 +0100
Subject: [PATCH] up

---
 certora/specs/GovernorFunctions.spec  | 4 ++--
 certora/specs/GovernorInvariants.spec | 8 ++------
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/certora/specs/GovernorFunctions.spec b/certora/specs/GovernorFunctions.spec
index b5e6d561c..3f361f2b0 100644
--- a/certora/specs/GovernorFunctions.spec
+++ b/certora/specs/GovernorFunctions.spec
@@ -1,7 +1,7 @@
 import "helpers.spec"
 import "Governor.helpers.spec"
 
-use invariant queuedImplySuccess
+use invariant queuedImplyVoteOver
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
@@ -233,7 +233,7 @@ rule execute_sideeffect(uint256 pId, env e, uint256 otherId) {
 rule cancel_liveness(uint256 pId, env e) {
     require nonpayable(e);
     require clockSanity(e);
-    requireInvariant queuedImplySuccess(pId);
+    requireInvariant queuedImplyVoteOver(pId);
 
     uint8 stateBefore = state(e, pId);
 
diff --git a/certora/specs/GovernorInvariants.spec b/certora/specs/GovernorInvariants.spec
index 7bbb5bf8b..c1676e449 100644
--- a/certora/specs/GovernorInvariants.spec
+++ b/certora/specs/GovernorInvariants.spec
@@ -91,12 +91,8 @@ invariant queuedImplyCreated(uint pId)
         }
     }
 
-invariant queuedImplyVoteOverAndSuccessful(env e, uint pId)
-    isQueued(pId) => (
-        quorumReached(pId) &&
-        voteSucceeded(pId) &&
-        proposalDeadline(pId) < clock(e)
-    )
+invariant queuedImplyVoteOver(env e, uint pId)
+    isQueued(pId) => proposalDeadline(pId) < clock(e)
     {
         preserved {
             require clockSanity(e);