From 5888bee85324562e6337f1f128ed85c1e084a7ab Mon Sep 17 00:00:00 2001
From: Michael George <mdgeorge@cs.cornell.edu>
Date: Thu, 2 Dec 2021 15:16:26 -0500
Subject: [PATCH] fixed executeOnly rule

---
 certora/specs/GovernorBase.spec | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index 7cec399c2..a7279b1ef 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -318,17 +318,15 @@ rule allFunctionsRevertIfCanceled(method f) filtered {
 /*
  * Proposal can be switched to executed only via execute() function
  */
-rule executedOnlyAfterExecuteFunc(address[] targets, uint256[] values, bytes[] calldatas, bytes32 descriptionHash, method f) filtered {
-    f -> f.selector != queue(address[],uint256[],bytes[],bytes32).selector
-} {
+rule executedOnlyAfterExecuteFunc(address[] targets, uint256[] values, bytes[] calldatas, bytes32 descriptionHash, method f) {
     env e; calldataarg args;
     uint256 pId;
     bool executedBefore = isExecuted(pId);
     require(!executedBefore);
 
     helperFunctionsWithRevert(pId, f, e);
-    require(!lastReverted);
 
     bool executedAfter = isExecuted(pId);
-    assert(executedAfter != executedBefore, "executed property did not change");
+    assert(executedAfter != executedBefore => f.selector == execute(address[], uint256[], bytes[], bytes32).selector, "isExecuted only changes in the execute method");
 }
+