Disabling a condition for CI because of timeout.

aptos-labs · Mar 12, 2024 · 5584cde · 5584cde
1 parent 447f486
commit 5584cde
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 3 deletions.
diff --git a/aptos-move/framework/aptos-framework/doc/reconfiguration_with_dkg.md b/aptos-move/framework/aptos-framework/doc/reconfiguration_with_dkg.md
@@ -157,8 +157,10 @@ Abort if no DKG is in progress.
 <pre><code><b>requires</b> <a href="chain_status.md#0x1_chain_status_is_operating">chain_status::is_operating</a>();
 <b>include</b> <a href="stake.md#0x1_stake_ResourceRequirement">stake::ResourceRequirement</a>;
 <b>include</b> <a href="stake.md#0x1_stake_GetReconfigStartTimeRequirement">stake::GetReconfigStartTimeRequirement</a>;
-<b>include</b> <a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features_spec_periodical_reward_rate_decrease_enabled">features::spec_periodical_reward_rate_decrease_enabled</a>() ==&gt; <a href="staking_config.md#0x1_staking_config_StakingRewardsConfigEnabledRequirement">staking_config::StakingRewardsConfigEnabledRequirement</a>;
+<b>include</b> <a href="../../aptos-stdlib/../move-stdlib/doc/features.md#0x1_features_spec_periodical_reward_rate_decrease_enabled">features::spec_periodical_reward_rate_decrease_enabled</a>(
+) ==&gt; <a href="staking_config.md#0x1_staking_config_StakingRewardsConfigEnabledRequirement">staking_config::StakingRewardsConfigEnabledRequirement</a>;
 <b>aborts_if</b> <b>false</b>;
+<b>pragma</b> verify_duration_estimate = 600;
 </code></pre>
 
 

diff --git a/aptos-move/framework/aptos-framework/sources/reconfiguration_with_dkg.spec.move b/aptos-move/framework/aptos-framework/sources/reconfiguration_with_dkg.spec.move
@@ -9,8 +9,10 @@ spec aptos_framework::reconfiguration_with_dkg {
         requires chain_status::is_operating();
         include stake::ResourceRequirement;
         include stake::GetReconfigStartTimeRequirement;
-        include features::spec_periodical_reward_rate_decrease_enabled() ==> staking_config::StakingRewardsConfigEnabledRequirement;
+        include features::spec_periodical_reward_rate_decrease_enabled(
+        ) ==> staking_config::StakingRewardsConfigEnabledRequirement;
         aborts_if false;
+        pragma verify_duration_estimate = 600; // TODO: set because of timeout (property proved).
     }
 
     spec finish(account: &signer) {
@@ -56,5 +58,4 @@ spec aptos_framework::reconfiguration_with_dkg {
         requires dkg::has_incomplete_session();
         aborts_if false;
     }
-
 }