test: remove now useless assumptions

morpho-org · Aug 12, 2024 · 54bac05 · 54bac05
1 parent a740591
commit 54bac05
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 5 deletions.
diff --git 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
@@ -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.