From e61ea55199b5b6efadf0ad7b439f86c9cdd38f2d Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Fri, 9 Aug 2024 00:25:11 +0200
Subject: [PATCH] removing fourth invariant from ...ArePreserved

---
 test/kontrol/VetoSignalling.t.sol | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/test/kontrol/VetoSignalling.t.sol b/test/kontrol/VetoSignalling.t.sol
index 6c7d10ef..e4ee5ac2 100644
--- a/test/kontrol/VetoSignalling.t.sol
+++ b/test/kontrol/VetoSignalling.t.sol
@@ -261,19 +261,19 @@ contract VetoSignallingTest is DualGovernanceSetUp {
                 // Establish third invariant
                 _vetoSignallingDeactivationInvariant(Mode.Assert, current);
             }
-            // Try establishing fourth invariant
-            if (!_vetoSignallingMaxDelayInvariant(Mode.Try, current)) {
-                // Assume third invariant if not already assumed
-                if (!assumedDeactivationInvariant) {
-                    _vetoSignallingDeactivationInvariant(Mode.Assume, previous);
-                }
-                // Assume fourth invariant if not already assumed
-                if (!assumedMaxDelayInvariant) {
-                    _vetoSignallingMaxDelayInvariant(Mode.Assume, previous);
-                }
-                // Establish fourth invariant
-                _vetoSignallingMaxDelayInvariant(Mode.Assert, current);
-            }
+            // // Try establishing fourth invariant
+            // if (!_vetoSignallingMaxDelayInvariant(Mode.Try, current)) {
+            //     // Assume third invariant if not already assumed
+            //     if (!assumedDeactivationInvariant) {
+            //         _vetoSignallingDeactivationInvariant(Mode.Assume, previous);
+            //     }
+            //     // Assume fourth invariant if not already assumed
+            //     if (!assumedMaxDelayInvariant) {
+            //         _vetoSignallingMaxDelayInvariant(Mode.Assume, previous);
+            //     }
+            //     // Establish fourth invariant
+            //     _vetoSignallingMaxDelayInvariant(Mode.Assert, current);
+            // }
             return;
         }
         vm.assume(currentState == State.VetoSignalling || currentState == State.VetoSignallingDeactivation);