removing fourth invariant from ...ArePreserved

runtimeverification · Aug 8, 2024 · e61ea55 · e61ea55
1 parent 18e0047
commit e61ea55
Showing 1 changed file with 13 additions and 13 deletions.
diff --git 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);