HarnessCleaning

certora/harnesses/ERC20VotesHarness.sol

@@ -25,13 +25,4 @@ contract ERC20VotesHarness is ERC20Votes {
         _getPastVotes[delegator][block.number] -= balanceOf(delegator);
         _getPastVotes[delegatee][block.number] += balanceOf(delegator);
     }
-
+}
-    /*
-    function getPastVotes(address account, uint256 blockNumber) public view virtual override returns (uint256) {
-        uint256 gpv = super.getPastVotes(account, blockNumber);
-        require (_getPastVotes[account][blockNumber] == gpv);
-        return gpv;
-    }
-    */
-
-}

certora/harnesses/WizardControlFirstPriority.sol

@@ -12,7 +12,7 @@ import "../../contracts/governance/extensions/GovernorProposalThreshold.sol";
 Wizard options:
 ProposalThreshhold = 10
 ERC20Votes
-TimelockCOntroller
+TimelockController
 */
 
 contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl {
@@ -77,6 +77,7 @@ contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, Gove
         return _proposalThreshold;                                          // HARNESS: parametric
     }
 
+    // original code, not harnessed
     // The following functions are overrides required by Solidity.
 
     function quorum(uint256 blockNumber)

certora/harnesses/WizardFirstTry.sol

@@ -68,6 +68,7 @@ contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, Gove
         return _votingPeriod;                                                   // HARNESS: parametric
     }
 
+    // original code, not harnessed
     // The following functions are overrides required by Solidity.
 
     function quorum(uint256 blockNumber)