From 1c52edbbd9f03eb094fb080d36bf573d61705037 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Fri, 1 Mar 2024 10:40:13 +0100
Subject: [PATCH] chore(Certora specs): comment out purposefully failing rule

We've introduced a rule that finds counter examples for all functions
that changes balances. This rule will always fail by definition, so
we're commenting it out to get CI green again.
---
 certora/specs/StakeManager.spec | 21 ++++++++++++---------
 1 file changed, 12 insertions(+), 9 deletions(-)

diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index caf0c7e..819b13b 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -107,15 +107,18 @@ rule revertsWhenNoMigration(method f) {
   assert isMigrationfunction(f) => reverted;
 }
 
-rule whoChangeERC20Balance(  method f ) filtered { f -> f.contract != staked }
-{
-  address user;
-  uint256 before = staked.balanceOf(user);
-  calldataarg args;
-  env e;
-  f(e,args);
-  assert before == staked.balanceOf(user);
-}
+// This rule is commented out as it's just a helper rule to easily see which
+// functions change the balance of the `StakeManager` contract.
+//
+// rule whoChangeERC20Balance(  method f ) filtered { f -> f.contract != staked }
+// {
+//   address user;
+//   uint256 before = staked.balanceOf(user);
+//   calldataarg args;
+//   env e;
+//   f(e,args);
+//   assert before == staked.balanceOf(user);
+// }
 
 rule epochOnlyIncreases {
   method f;