From 06baea7fa89f87e3320396553a1e6d4643d571d3 Mon Sep 17 00:00:00 2001
From: Hadrien Croubois <hadrien.croubois@gmail.com>
Date: Wed, 15 Mar 2023 23:28:50 +0100
Subject: [PATCH] up

---
 certora/specs/GovernorStates.spec | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/certora/specs/GovernorStates.spec b/certora/specs/GovernorStates.spec
index d601fc996..af6ffcf26 100644
--- a/certora/specs/GovernorStates.spec
+++ b/certora/specs/GovernorStates.spec
@@ -143,8 +143,14 @@ rule onlyVoteCanChangeQuorumReached(uint256 pId, env e, method f, calldataarg ar
 
     bool quorumReachedBefore = quorumReached(pId);
 
+    uint256 snapshot    = proposalSnapshot(pId);
+    uint256 totalSupply = token_getPastTotalSupply(snapshot);
+
     f(e, args);
 
+    // Needed because the prover doesn't understand the checkpoint properties of the voting token.
+    require clock(e) > snapshot => token_getPastTotalSupply(snapshot) == cache;
+
     assert quorumReached(pId) != quorumReachedBefore => (
         !quorumReachedBefore &&
         votingAll(f)