From c97107a604b605fbac68ac68ee11727e0737dfe7 Mon Sep 17 00:00:00 2001
From: Derek Sorensen <derek-certora@Dereks-MacBook-Pro.local>
Date: Wed, 18 Dec 2024 09:44:16 +0000
Subject: [PATCH] combine the two setup rules into one more concise rules

---
 certora/specs/v1.5/Setup.spec | 34 ++++++++--------------------------
 1 file changed, 8 insertions(+), 26 deletions(-)

diff --git a/certora/specs/v1.5/Setup.spec b/certora/specs/v1.5/Setup.spec
index ce0ca7f55..67217d450 100644
--- a/certora/specs/v1.5/Setup.spec
+++ b/certora/specs/v1.5/Setup.spec
@@ -16,10 +16,10 @@ methods {
 
 // ---- Rules ------------------------------------------------------------------
 
-/// @dev setup can only be called if threshold = 0
-/// @status Done: https://prover.certora.com/output/39601/202435585f914643abd02fe37b8d1fc5?anonymousKey=e74abb4876b18456b372d84e44ad78e3a22a0566
+/// @dev setup can only be called if threshold = 0 and setup sets threshold > 0 
+/// @status Done: https://prover.certora.com/output/39601/7849e9a464e042ea89bfe68fc226edbc?anonymousKey=5c1387afecb8bc86f23df3be5eb886a5cd82787f
 
-rule setupThresholdZero(
+rule setupThresholdZeroAndSetsPositiveThreshold(
         address[] _owners,
         uint256 _threshold,
         address to,
@@ -36,28 +36,10 @@ rule setupThresholdZero(
     setup(e,_owners,_threshold,to,data,fallbackHandler,
         paymentToken,payment,paymentReceiver);
 
-    assert (old_threshold == 0);
-}
-
-/// @dev setup sets threshold > 0 
-/// @status Done: https://prover.certora.com/output/39601/202435585f914643abd02fe37b8d1fc5?anonymousKey=e74abb4876b18456b372d84e44ad78e3a22a0566 
-
-rule setupSetsPositiveThreshold(
-        address[] _owners,
-        uint256 _threshold,
-        address to,
-        bytes data,
-        address fallbackHandler,
-        address paymentToken,
-        uint256 payment,
-        address paymentReceiver) {
-    env e;
-
-    // a successful call to setup
-    setup(e,_owners,_threshold,to,data,fallbackHandler,
-        paymentToken,payment,paymentReceiver);
-    
     uint256 new_threshold = getThreshold();
 
-    assert (new_threshold > 0);
-}
\ No newline at end of file
+    assert (
+        new_threshold >  0 &&
+        old_threshold == 0
+    );
+}