From 1c5eacc8283011e89d2ea0cd86e196e0ea79be7c Mon Sep 17 00:00:00 2001
From: axiongsupra <a.xiong@supraoracles.com>
Date: Thu, 28 Nov 2024 22:05:49 -0500
Subject: [PATCH] Enable post condition for `is_voting_closed`

---
 .../supra-framework/sources/multisig_voting.spec.move         | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/aptos-move/framework/supra-framework/sources/multisig_voting.spec.move b/aptos-move/framework/supra-framework/sources/multisig_voting.spec.move
index 0dd5d54df0b76..adedd3f7b7266 100644
--- a/aptos-move/framework/supra-framework/sources/multisig_voting.spec.move
+++ b/aptos-move/framework/supra-framework/sources/multisig_voting.spec.move
@@ -214,7 +214,7 @@ spec supra_framework::multisig_voting {
         pragma aborts_if_is_partial = true;
         include AbortsIfNotContainProposalID<ProposalType>;
         // aborts_if !exists<timestamp::CurrentTimeMicroseconds>(@supra_framework);
-        // ensures result == spec_is_voting_closed<ProposalType>(voting_forum_address, proposal_id);
+        ensures result == spec_is_voting_closed<ProposalType>(voting_forum_address, proposal_id);
     }
 
     spec can_be_resolved_early {
@@ -414,7 +414,7 @@ spec supra_framework::multisig_voting {
     spec fun spec_is_voting_closed<ProposalType: store>(voting_forum_address: address, proposal_id: u64): bool {
         let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address);
         let proposal = table::spec_get(voting_forum.proposals, proposal_id);
-        is_voting_period_over(proposal)
+        spec_can_be_resolved_early(proposal)||is_voting_period_over(proposal)
     }
 
     spec fun spec_can_be_resolved_early<ProposalType: store>(proposal: Proposal<ProposalType>): bool {