different prover args for sanity checks.

Author: raz-certora

certora/confs/ConsistentStateNotInQueue.conf

@@ -6,7 +6,7 @@
     "global_timeout": "7200",
     "smt_timeout" : "6000",
     "parametric_contracts": "EulerEarnHarness",
-    "rule_sanity": "none",
+    "rule_sanity": "basic",
     "rule" : "notInWithdrawQThenNoApproval",
     "files": [
         "certora/harnesses/EulerEarnHarness.sol",
@@ -52,6 +52,7 @@
     "contract_recursion_limit": "1",
     "process": "emv",
     "prover_args": [
-        "-cvlFunctionRevert true"
+        "-cvlFunctionRevert true",
+        "DISABLE_SPLIT"
     ]
 }

certora/confs/Solvency.conf

@@ -5,7 +5,7 @@
     "rule": [
         "TotalAssetsMoreThanSupplyAndFees"
     ],
-    "rule_sanity": "none",
+    "rule_sanity": "basic",
     "loop_iter": "1",
     "optimistic_loop": true,
     "global_timeout": "7200",
@@ -56,6 +56,7 @@
     "optimistic_summary_recursion": true,
     "process": "emv",
     "prover_args": [
-        "-cvlFunctionRevert true"
+        "-cvlFunctionRevert true",
+        "DISABLE_SPLIT"
     ]
 }

certora/confs/SolvencyInternal.conf

@@ -3,7 +3,7 @@
     "verify": "EulerEarnHarness:certora/specs/SolvencyInternal.spec",
     "msg": "Euler Earn - internal solvency",
     "multi_assert_check" : true,
-    "rule_sanity": "none",
+    "rule_sanity": "basic",
     "loop_iter": "1",
     "optimistic_loop": true,
     "global_timeout": "7200",
@@ -54,11 +54,7 @@
     "optimistic_summary_recursion" : true,
     "process": "emv",
     "prover_args": [
-        //"-verifyCache ",
-        //"-verifyTACDumps",
-        //"-testMode",
-        //"-checkRuleDigest",
-        //"-callTraceHardFail on",
-        "-cvlFunctionRevert true"
+        "-cvlFunctionRevert true",
+        "DISABLE_SPLIT"
     ]
 }

certora/confs/TimelockRemovableTime.conf

@@ -6,7 +6,7 @@
     "global_timeout": "7200",
     "smt_timeout" : "6000",
     "parametric_contracts": "EulerEarnHarness",
-    "rule_sanity": "none",
+    "rule_sanity": "basic",
     "rule" : "removableTime",
     "files": [
         "certora/harnesses/EulerEarnHarness.sol",
@@ -52,6 +52,7 @@
     "contract_recursion_limit": "1",
     "process": "emv",
     "prover_args": [
-        "-cvlFunctionRevert true"
+        "-cvlFunctionRevert true",
+        "DISABLE_SPLIT"
     ]
 }