From 54bac0536711c188555cba365442aa362422a195 Mon Sep 17 00:00:00 2001
From: MathisGD <mathis@morpho.xyz>
Date: Mon, 12 Aug 2024 11:03:24 +0200
Subject: [PATCH] test: remove now useless assumptions

---
 certora/specs/Liveness.spec      | 1 -
 certora/specs/PendingValues.spec | 4 ----
 2 files changed, 5 deletions(-)

diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
index 54156f75..8612ae72 100644
--- a/certora/specs/Liveness.spec
+++ b/certora/specs/Liveness.spec
@@ -53,7 +53,6 @@ rule canForceRemoveMarket(MetaMorphoHarness.MarketParams marketParams) {
     assert !lastReverted;
 
     require e3.msg.value == 0;
-    requireInvariant timelockInRange();
     // Safe require as it corresponds to some time very far into the future.
     require e3.block.timestamp < 2^63;
     // Safe require as it corresponds to some time very far into the past.
diff --git a/certora/specs/PendingValues.spec b/certora/specs/PendingValues.spec
index 5adfd77b..b1e65a05 100644
--- a/certora/specs/PendingValues.spec
+++ b/certora/specs/PendingValues.spec
@@ -12,7 +12,6 @@ invariant noBadPendingTimelock()
     hasNoBadPendingTimelock()
 {
     preserved with (env e) {
-        requireInvariant timelockInRange();
         // Safe require as it corresponds to some time very far into the future.
         require e.block.timestamp < 2^63;
         // Safe require as it corresponds to some time very far into the past.
@@ -26,7 +25,6 @@ invariant smallerPendingTimelock()
 {
     preserved with (env e) {
         requireInvariant pendingTimelockInRange();
-        requireInvariant timelockInRange();
         // Safe require as it corresponds to some time very far into the past.
         require e.block.timestamp > 0;
     }
@@ -43,7 +41,6 @@ invariant noBadPendingCap(MetaMorphoHarness.Id id)
     hasNoBadPendingCap(id)
 {
     preserved with (env e) {
-        requireInvariant timelockInRange();
         // Safe require as it corresponds to some time very far into the future.
         require e.block.timestamp < 2^63;
         // Safe require as it corresponds to some time very far into the past.
@@ -74,7 +71,6 @@ invariant noBadPendingGuardian()
     hasNoBadPendingGuardian()
 {
     preserved with (env e) {
-        requireInvariant timelockInRange();
         // Safe require as it corresponds to some time very far into the future.
         require e.block.timestamp < 2^63;
         // Safe require as it corresponds to some time very far into the past.