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)); + } + }