From 0cbb98b92c6be44b21cbad735868302137cfaf70 Mon Sep 17 00:00:00 2001
From: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Date: Thu, 18 Nov 2021 16:42:32 +0200
Subject: [PATCH] uncommenting hook for oneUserVotesInCast

---
 certora/specs/GovernorCountingSimple.spec | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec
index 59475a529..949cdc876 100644
--- a/certora/specs/GovernorCountingSimple.spec
+++ b/certora/specs/GovernorCountingSimple.spec
@@ -25,10 +25,10 @@ ghost hasVoteGhost(uint256) returns uint256 {
     init_state axiom forall uint256 pId. hasVoteGhost(pId) == 0;
 }
 
-//hook Sstore _proposalVotes[KEY uint256 pId].hasVoted[KEY address user] bool current_voting_State (bool old_voting_state) STORAGE{
-//    havoc hasVoteGhost assuming forall uint256 p. ((p == pId && current_voting_State && !old_voting_state) ? (hasVoteGhost@new(p) == hasVoteGhost@old(p) + 1)  :
-//                                                  (hasVoteGhost@new(p) == hasVoteGhost@old(p)));
-//}
+hook Sstore _proposalVotes[KEY uint256 pId].hasVoted[KEY address user] bool current_voting_State (bool old_voting_state) STORAGE{
+   havoc hasVoteGhost assuming forall uint256 p. ((p == pId && current_voting_State && !old_voting_state) ? (hasVoteGhost@new(p) == hasVoteGhost@old(p) + 1)  :
+                                                 (hasVoteGhost@new(p) == hasVoteGhost@old(p)));
+}
 
 ghost sum_all_votes_power() returns uint256 {
 	init_state axiom sum_all_votes_power() == 0;