diff --git a/certora/confs/LossFactor.conf b/certora/confs/LossFactor.conf
index dd3277bc..07d3d193 100644
--- a/certora/confs/LossFactor.conf
+++ b/certora/confs/LossFactor.conf
@@ -7,18 +7,21 @@
   "solc": "solc-0.8.34",
   "solc_via_ir": true,
   "solc_evm_version": "osaka",
-  "optimistic_loop": true,
   "loop_iter": 2,
+  "optimistic_loop": true,
   "optimistic_hashing": true,
   "hashing_length_bound": 2048,
   "smt_timeout": 7200,
   "prover_args": [
-    "-splitParallel true",
     "-destructiveOptimizations twostage",
+    "-smt_initialSplitDepth 4",
+    "-depth 10",
+    "-mediumTimeout 2",
     "-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}]"
   ],
   "split_rules": [
-    "liquidateLossFactorDoesNotRevert"
+    "liquidateLossFactorDoesNotRevert",
+    "onlyLiquidateChangesMarketLossFactor"
   ],
   "msg": "Loss Factor"
 }
diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf
index 1940cfb8..2a8ce9aa 100644
--- a/certora/confs/Reentrancy.conf
+++ b/certora/confs/Reentrancy.conf
@@ -3,8 +3,20 @@
     "src/Midnight.sol"
   ],
   "prover_args": [
-    "-enableStorageSplitting false",
-    "-destructiveOptimizations twostage"
+    "-enableStorageSplitting",
+    "false",
+    "-destructiveOptimizations",
+    "twostage",
+    "-oldSplitParallel",
+    "true",
+    "-dontStopAtFirstSplitTimeout",
+    "true",
+    "-splitParallelTimelimit",
+    "7000",
+    "-splitParallelInitialDepth",
+    "3",
+    "-numOfParallelSplits",
+    "7"
   ],
   "solc": "solc-0.8.34",
   "solc_via_ir": true,
diff --git a/certora/confs/Role.conf b/certora/confs/Role.conf
index af701432..f9d175e6 100644
--- a/certora/confs/Role.conf
+++ b/certora/confs/Role.conf
@@ -12,9 +12,11 @@
   "optimistic_hashing": true,
   "hashing_length_bound": 2048,
   "prover_args": [
-    "-s",
-    "[z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5}]",
-    "-splitParallel true"
+    "-destructiveOptimizations twostage",
+    "-mediumTimeout 20",
+    "-lowTimeout 20",
+    "-tinyTimeout 20",
+    "-depth 20"
   ],
   "msg": "Role Safety and Liveness"
 }
diff --git a/certora/confs/SplitDoesNotPunishMakerOrFavorTaker.conf b/certora/confs/SplitDoesNotPunishMakerOrFavorTaker.conf
index 2a3b952b..c72bb033 100644
--- a/certora/confs/SplitDoesNotPunishMakerOrFavorTaker.conf
+++ b/certora/confs/SplitDoesNotPunishMakerOrFavorTaker.conf
@@ -11,15 +11,13 @@
   "loop_iter": 2,
   "optimistic_hashing": true,
   "hashing_length_bound": 1024,
-  "smt_timeout": 7200,
+  "smt_timeout": 1800,
   "prover_args": [
-    "-depth 10",
-    "-mediumTimeout 60",
-    "-splitParallel true",
-    "-smt_initialSplitDepth 2",
     "-destructiveOptimizations twostage",
-    "-s",
-    "[z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},cvc5:def,bitwuzla:def]"
+    "-backendStrategy singleRace",
+    "-smt_useLIA false",
+    "-smt_useNIA true",
+    "-depth 0"
   ],
   "msg": "Split Does Not Punish Maker Or Favor Taker"
 }
diff --git a/certora/confs/TakeAmountsLibInvertibility.conf b/certora/confs/TakeAmountsLibInvertibility.conf
index a42d09f0..22e359e3 100644
--- a/certora/confs/TakeAmountsLibInvertibility.conf
+++ b/certora/confs/TakeAmountsLibInvertibility.conf
@@ -13,10 +13,14 @@
   "optimistic_loop": true,
   "loop_iter": 2,
   "prover_args": [
-    "-destructiveOptimizations twostage",
-    "-splitParallel true",
-    "-splitParallelInitialDepth 4",
-    "-splitParallelTimelimit 7200"
+    "-destructiveOptimizations",
+    "twostage",
+    "-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}]",
+    "-splitParallel",
+    "true",
+    "-dontStopAtFirstSplitTimeout",
+    "true"
   ],
   "msg": "Midnight TakeAmountsLib Invertibility"
 }