From c819e0b06358ca2bc5f28da7b10070dea70a46c8 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Mon, 8 Nov 2021 17:57:53 +0200
Subject: [PATCH] added ghost and counter implementation for castWithReason and
 castBySig

---
 certora/harnesses/GovernorHarness.sol | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/certora/harnesses/GovernorHarness.sol b/certora/harnesses/GovernorHarness.sol
index 880f706d6..e6182ff8e 100644
--- a/certora/harnesses/GovernorHarness.sol
+++ b/certora/harnesses/GovernorHarness.sol
@@ -120,8 +120,13 @@ contract GovernorHarness is Governor {
         string calldata reason
     ) public virtual override returns (uint256) {
         address voter = _msgSender();
-        counter_vote_power_by_id[proposalId] += _castVote(proposalId, voter, support, reason);
-        return _castVote(proposalId, voter, support, reason);
+        // 2)
+        ghost_vote_power_by_id[proposalId] = _castVote(proposalId, voter, support, reason);
+        
+        // 1)
+        counter_vote_power_by_id[proposalId] += ghost_vote_power_by_id[proposalId];
+
+        return ghost_vote_power_by_id[proposalId];
     }
 
     function castVoteBySig(
@@ -137,7 +142,12 @@ contract GovernorHarness is Governor {
             r,
             s
         );
-        counter_vote_power_by_id[proposalId] += _castVote(proposalId, voter, support, "");
-        return _castVote(proposalId, voter, support, "");
+        // 2)
+        ghost_vote_power_by_id[proposalId] = _castVote(proposalId, voter, support, "");
+
+        // 1)
+        counter_vote_power_by_id[proposalId] += ghost_vote_power_by_id[proposalId];
+
+        return ghost_vote_power_by_id[proposalId];
     }
 }
\ No newline at end of file