From e9f0077488c976994d3aaf45a5d004e83f0d07fc Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Mon, 4 Mar 2024 16:19:45 +0100
Subject: [PATCH] fix(StakeManager.spec): ensure `revertsWhenNoMigration`
 passes

The were changes in the contracts that caused this rule to fail.
Namely `migrateTo` shouldn't be reverting so this as been removed from
the rule and `transferNonPending` has been added as it was missing.
---
 certora/specs/StakeManager.spec | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/certora/specs/StakeManager.spec b/certora/specs/StakeManager.spec
index bd02388..24eff29 100644
--- a/certora/specs/StakeManager.spec
+++ b/certora/specs/StakeManager.spec
@@ -27,8 +27,8 @@ function getAccountBalance(address addr) returns uint256 {
 
 function isMigrationfunction(method f) returns bool {
   return
-          f.selector == sig:migrateFrom(address,bool,StakeManager.Account).selector ||
-          f.selector == sig:migrateTo(bool).selector;
+          f.selector == sig:migrateTo(bool).selector ||
+          f.selector == sig:transferNonPending().selector;
 }
 
 /*  assume that migration is zero, causing the verification to take into account only