diff --git a/certora/scripts/Governor.sh b/certora/scripts/Governor.sh index 97486c2fa..8b177300d 100755 --- a/certora/scripts/Governor.sh +++ b/certora/scripts/Governor.sh @@ -4,4 +4,6 @@ certoraRun certora/harnesses/GovernorHarness.sol \ --staging \ --msg $1 \ --disableLocalTypeChecking \ - --rule voteStartBeforeVoteEnd \ No newline at end of file + --optimistic_loop \ + --settings -copyLoopUnroll=4 + --rule sanityCheckVoteStart diff --git a/certora/scripts/sanity.sh b/certora/scripts/sanity.sh index 0da31d15e..7ffaf52f7 100644 --- a/certora/scripts/sanity.sh +++ b/certora/scripts/sanity.sh @@ -5,7 +5,8 @@ do echo ${file%.*} certoraRun certora/harnesses/$file \ --verify ${file%.*}:certora/specs/sanity.spec "$@" \ - --solc solc8.0 \ - --staging \ - --msg "sanity ${file}" + --solc solc8.0 --staging \ + --optimistic_loop \ + --msg "checking sanity on ${file%.*}" + --settings -copyLoopUnroll=4 done \ No newline at end of file diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index b54f8c0e8..17a37b88e 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -32,7 +32,6 @@ hook Sload uint64 value _proposals[KEY uint256 pId].voteStart._deadline STORAGE require proposalVoteStart(pId) == value; } - hook Sstore _proposals[KEY uint256 pId].voteEnd._deadline uint64 newValue STORAGE { havoc proposalVoteEnd assuming ( proposalVoteEnd@new(pId) == newValue