diff --git a/certora/scripts/WizardControlFirstPriority.sh b/certora/scripts/WizardControlFirstPriority.sh index 18fccf804..3f367de2c 100644 --- a/certora/scripts/WizardControlFirstPriority.sh +++ b/certora/scripts/WizardControlFirstPriority.sh @@ -2,6 +2,7 @@ certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardContr --link WizardControlFirstPriority:token=ERC20VotesHarness \ --verify WizardControlFirstPriority:certora/specs/GovernorBase.spec \ --solc solc8.2 \ + --disableLocalTypeChecking \ --staging shelly/forSasha \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ diff --git a/certora/scripts/verifyAll.sh b/certora/scripts/verifyAll.sh index 864aa47bd..6a7a42fa9 100644 --- a/certora/scripts/verifyAll.sh +++ b/certora/scripts/verifyAll.sh @@ -4,27 +4,30 @@ do do contractFile=$(basename $contract) specFile=$(basename $spec) - echo "Processing ${contractFile%.*} with $specFile" - if [[ "${contractFile%.*}" = *"WizardControl"* ]]; + if [[ "${specFile%.*}" != "RulesInProgress" ]]; then - certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ - --link ${contractFile%.*}:token=ERC20VotesHarness \ - --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ - --solc solc8.2 \ - --staging shelly/forSasha \ - --disableLocalTypeChecking \ - --optimistic_loop \ - --settings -copyLoopUnroll=4 \ - --msg "checking $specFile on ${contractFile%.*}" - else - certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ - --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ - --solc solc8.2 \ - --staging shelly/forSasha \ - --disableLocalTypeChecking \ - --optimistic_loop \ - --settings -copyLoopUnroll=4 \ - --msg "checking $specFile on ${contractFile%.*}" + echo "Processing ${contractFile%.*} with $specFile" + if [[ "${contractFile%.*}" = *"WizardControl"* ]]; + then + certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ + --link ${contractFile%.*}:token=ERC20VotesHarness \ + --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ + --solc solc8.2 \ + --staging shelly/forSasha \ + --disableLocalTypeChecking \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + --msg "checking $specFile on ${contractFile%.*}" + else + certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ + --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ + --solc solc8.2 \ + --staging shelly/forSasha \ + --disableLocalTypeChecking \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + --msg "checking $specFile on ${contractFile%.*}" + fi fi done done \ No newline at end of file