From 2e1d0b375695c39fc0e2a61093099471719ebdc5 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Tue, 9 May 2023 10:31:17 +0200 Subject: [PATCH] fix spec file --- certora/specs/GovernorStates.spec | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec index eb0f103f9..bb6a6f524 100644 --- a/certora/specs/GovernorStates.spec +++ b/certora/specs/GovernorStates.spec @@ -5,8 +5,8 @@ import "GovernorInvariants.spec" use invariant proposalStateConsistency use invariant votesImplySnapshotPassed -definition assumedSafeOrDuplicateOrDuplicate(method f) returns bool = - assumedSafeOrDuplicate(f) +definition assumedSafeOrDuplicate(method f) returns bool = + assumedSafe(f) || f.selector == castVoteWithReason(uint256,uint8,string).selector || f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector || f.selector == castVoteBySig(uint256,uint8,uint8,bytes32,bytes32).selector @@ -19,7 +19,7 @@ definition assumedSafeOrDuplicateOrDuplicate(method f) returns bool = */ invariant stateConsistency(env e, uint256 pId) state(e, pId) == safeState(e, pId) - filtered { f -> !assumedSafeOrDuplicateOrDuplicate(f); } + filtered { f -> !assumedSafeOrDuplicate(f) } rule stateDomain(env e, uint256 pId) { uint8 result = safeState(e, pId);