diff --git a/certora/scripts/passes/verifyGPLQ_deadlineCantBeUnextended.sh b/certora/scripts/passes/verifyGPLQ_deadlineCantBeUnextended.sh index a28e75967..ae3b2a55e 100644 --- a/certora/scripts/passes/verifyGPLQ_deadlineCantBeUnextended.sh +++ b/certora/scripts/passes/verifyGPLQ_deadlineCantBeUnextended.sh @@ -7,6 +7,7 @@ certoraRun \ --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \ --link GovernorFullHarness:token=ERC20VotesHarness \ --optimistic_loop \ + --optimistic_hashing \ --rule deadlineCantBeUnextended \ --loop_iter 1 \ $@ diff --git a/certora/scripts/passes/verifyGPLQ_proposalInOneState.sh b/certora/scripts/passes/verifyGPLQ_proposalInOneState.sh index 94754778e..defb01802 100644 --- a/certora/scripts/passes/verifyGPLQ_proposalInOneState.sh +++ b/certora/scripts/passes/verifyGPLQ_proposalInOneState.sh @@ -7,7 +7,8 @@ certoraRun \ --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \ --link GovernorFullHarness:token=ERC20VotesHarness \ --optimistic_loop \ + --optimistic_hashing \ --rule proposalInOneState \ - --settings -t=1000 \ --loop_iter 1 \ + --settings -t=1000 \ $@ diff --git a/certora/scripts/passes/verifyGPLQ_quorumReachedEffect.sh b/certora/scripts/passes/verifyGPLQ_quorumReachedEffect.sh index 2cbebae8f..06c3da897 100644 --- a/certora/scripts/passes/verifyGPLQ_quorumReachedEffect.sh +++ b/certora/scripts/passes/verifyGPLQ_quorumReachedEffect.sh @@ -7,6 +7,7 @@ certoraRun \ --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \ --link GovernorFullHarness:token=ERC20VotesHarness \ --optimistic_loop \ + --optimistic_hashing \ --rule quorumReachedEffect \ --loop_iter 1 \ $@ diff --git a/certora/scripts/passes/verifyGovernor.sh b/certora/scripts/passes/verifyGovernor.sh index 02d2b3118..fe1e0387d 100644 --- a/certora/scripts/passes/verifyGovernor.sh +++ b/certora/scripts/passes/verifyGovernor.sh @@ -11,5 +11,6 @@ certoraRun \ --verify GovernorHarness:certora/specs/GovernorBase.spec \ --link GovernorHarness:token=ERC20VotesHarness \ --optimistic_loop \ + --optimistic_hashing \ --settings -copyLoopUnroll=4 \ $@ \ No newline at end of file diff --git a/certora/scripts/passes/verifyGovernorCountingSimple.sh b/certora/scripts/passes/verifyGovernorCountingSimple.sh index b774d5fc5..070d7379a 100644 --- a/certora/scripts/passes/verifyGovernorCountingSimple.sh +++ b/certora/scripts/passes/verifyGovernorCountingSimple.sh @@ -8,5 +8,6 @@ certoraRun \ --verify GovernorHarness:certora/specs/GovernorCountingSimple.spec \ --link GovernorHarness:token=ERC20VotesHarness \ --optimistic_loop \ + --optimistic_hashing \ --settings -copyLoopUnroll=4 \ $@