From dacd39b2c208692a082405ea7fbe28dcce931e9f Mon Sep 17 00:00:00 2001
From: axiongsupra <a.xiong@supraoracles.com>
Date: Tue, 3 Dec 2024 21:55:24 -0500
Subject: [PATCH] Enable verification for `vest_transfer` and
 `remove_shareholder`

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

diff --git a/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move b/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move
index 609e70791d14f..f3d526ebd1545 100644
--- a/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move
+++ b/aptos-move/framework/supra-framework/sources/vesting_without_staking.spec.move
@@ -108,7 +108,7 @@ spec supra_framework::vesting_without_staking {
 
     spec vest_transfer {
         // TODO(fa_migration)
-        pragma verify = false;
+        pragma verify = true;
         let amount = min(vesting_record.left_amount, fixed_point32::spec_multiply_u64(vesting_record.init_amount, vesting_fraction));
         // Ensure that the amount is substracted from the left_amount
         ensures vesting_record.left_amount == old(vesting_record.left_amount) - amount;
@@ -126,7 +126,7 @@ spec supra_framework::vesting_without_staking {
 
     spec remove_shareholder {
         // TODO(fa_migration)
-        pragma verify = false;
+        pragma verify = true;
         pragma aborts_if_is_partial = true;
         include AdminAborts;
         let vesting_contract = global<VestingContract>(contract_address);