diff --git a/certora/scripts/WizardFirstTry.sh b/certora/scripts/WizardFirstTry.sh index 8aa46e8cb..361814d8b 100644 --- a/certora/scripts/WizardFirstTry.sh +++ b/certora/scripts/WizardFirstTry.sh @@ -3,6 +3,6 @@ certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirst --solc solc8.2 \ --staging shelly/forSasha \ --optimistic_loop \ + --disableLocalTypeChecking \ --settings -copyLoopUnroll=4 \ - --rule allFunctionsRevertIfCanceled \ - --msg "$1" \ No newline at end of file + --msg "$1" diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index a7279b1ef..798d63381 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -25,8 +25,8 @@ methods { getVotes(address, uint256) returns uint256 => DISPATCHER(true) - erc20votes.getPastTotalSupply(uint256) returns uint256 - erc20votes.getPastVotes(address, uint256) returns uint256 + getPastTotalSupply(uint256) returns uint256 => NONDET + getPastVotes(address, uint256) returns uint256 => NONDET //scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => DISPATCHER(true) //executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true) @@ -281,7 +281,7 @@ rule allFunctionsRevertIfExecuted(method f) filtered { f -> && f.selector != updateTimelock(address).selector && f.selector != updateQuorumNumerator(uint256).selector && f.selector != queue(address[],uint256[],bytes[],bytes32).selector - && f.selector != __acceptAdmin().selector + && f.selector != 0xb9a61961 // __acceptAdmin() } { env e; calldataarg args; uint256 pId; @@ -302,7 +302,7 @@ rule allFunctionsRevertIfCanceled(method f) filtered { && f.selector != updateTimelock(address).selector && f.selector != updateQuorumNumerator(uint256).selector && f.selector != queue(address[],uint256[],bytes[],bytes32).selector - && f.selector != __acceptAdmin().selector + && f.selector != 0xb9a61961 // __acceptAdmin() } { env e; calldataarg args; uint256 pId;