From 5bc7b564e89475bb6b0adfee518d594496e961f4 Mon Sep 17 00:00:00 2001
From: Ricardo Guilherme Schmidt <3esmit@gmail.com>
Date: Wed, 13 Nov 2024 18:27:32 -0300
Subject: [PATCH] choe(MaxMPRule.conf): remove args and settings

---
 certora/confs/MaxMPRule.conf | 48 ++++++++++++++----------------------
 1 file changed, 18 insertions(+), 30 deletions(-)

diff --git a/certora/confs/MaxMPRule.conf b/certora/confs/MaxMPRule.conf
index f37d5f3..315d95f 100644
--- a/certora/confs/MaxMPRule.conf
+++ b/certora/confs/MaxMPRule.conf
@@ -1,32 +1,20 @@
 {
-	"files": [
-		"contracts/StakeManager.sol",
+  "files": [
+    "contracts/StakeManager.sol",
     "certora/helpers/ExpiredStakeStorageA.sol",
-		"certora/helpers/ERC20A.sol"
-	],
-	"global_timeout": "7200",
-	"link": [
-		"StakeManager:STAKING_TOKEN=ERC20A",
-    "StakeManager:expiredStakeStorage=ExpiredStakeStorageA",
-	],
-	"loop_iter": "3",
-	"msg": "Z3 random seeds",
-	"optimistic_loop": true,
-	"packages": [
-		"forge-std=lib/forge-std/src",
-		"@openzeppelin=lib/openzeppelin-contracts"
-	],
-	"process": "emv",
-	"prover_args": [
-		" -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]"
-	],
-	"prover_version": "master",
-	"rule": [
-		"MPcantBeGreaterThanMaxMP"
-	],
-  "rule_sanity": "none",
-	"smt_timeout": "7200",
-	"verify": "StakeManager:certora/specs/MaxMPRule.spec"
-}
-
-
+    "certora/helpers/ERC20A.sol"
+  ],
+  "link": [
+    "StakeManager:REWARD_TOKEN=ERC20A",
+    "StakeManager:expiredStakeStorage=ExpiredStakeStorageA"
+  ],
+  "msg": "Verifying StakeManager.sol maxMP rule",
+  "rule_sanity": "basic",
+  "verify": "StakeManager:certora/specs/MaxMPRule.spec",
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "packages": [
+    "forge-std=lib/forge-std/src",
+    "@openzeppelin=lib/openzeppelin-contracts"
+  ]
+}
\ No newline at end of file