From 37a4975544e34194134432ccdeeb0a0fd07adcb7 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Mon, 8 Nov 2021 17:51:28 +0200
Subject: [PATCH] fixed function revert if executed

---
 certora/specs/GovernorBase.spec | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec
index ba8b9c93e..ac1dfb6b3 100644
--- a/certora/specs/GovernorBase.spec
+++ b/certora/specs/GovernorBase.spec
@@ -61,7 +61,13 @@ invariant cannotSetIfCanceled(uint256 pId)
  * No functions should be allowed to run after a job is deemed as executed
  */
 invariant cannotSetIfExecuted(uint256 pId)
-    isExecuted(pId) => lastReverted == true
+    isExecuted(pId) => lastReverted == true 
+    {
+        preserved execute(address[] targets, uint256[] values, bytes[] calldatas, bytes32 descriptionHash) with (env e)
+        {
+            require(isExecuted(pId));
+        }
+    }