diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf
index b81daf37b..cff95424a 100644
--- a/certora/confs/ConsistentState.conf
+++ b/certora/confs/ConsistentState.conf
@@ -6,6 +6,7 @@
   "solc": "solc-0.8.19",
   "verify": "MorphoHarness:certora/specs/ConsistentState.spec",
   "rule_sanity": "basic",
+  "smt_timeout": 3600,
   "server": "production",
   "msg": "Morpho Blue Consistent State"
 }
diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec
index a724242d2..57f8073fd 100644
--- a/certora/specs/ConsistentState.spec
+++ b/certora/specs/ConsistentState.spec
@@ -24,6 +24,9 @@ methods {
     function Util.wad() external returns (uint256) envfree;
     function Util.libId(MorphoHarness.MarketParams) external returns (MorphoHarness.Id) envfree;
 
+    // Over-approximate pure function.
+    function UtilsLib.min(uint256, uint256) internal returns (uint256) => NONDET;
+
     function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => HAVOC_ECF;
 
     function SafeTransferLib.safeTransfer(address token, address to, uint256 value) internal => summarySafeTransferFrom(token, currentContract, to, value);
diff --git a/foundry.lock b/foundry.lock
index eb1f7aaf1..d186590c5 100644
--- a/foundry.lock
+++ b/foundry.lock
@@ -1,8 +1,5 @@
 {
   "lib/forge-std": {
     "rev": "2f112697506eab12d433a65fdc31a639548fe365"
-  },
-  "lib/halmos-cheatcodes": {
-    "rev": "a02072cd5eb8560d00c3f4a73b27831ec6e3137e"
   }
 }
\ No newline at end of file
diff --git a/foundry.toml b/foundry.toml
index 395accf4c..df6972f35 100644
--- a/foundry.toml
+++ b/foundry.toml
@@ -21,12 +21,10 @@ exclude_lints = [
     "unaliased-plain-import",
     "asm-keccak256",
     "unwrapped-modifier-logic",
+    "unsafe-typecast",
+    "block-timestamp",
 ]
-ignore = [
-    'test/**/*.sol'
-]
+ignore = ['test/**/*.sol']
 
 [profile.no_via_ir]
-via-ir = false
-
-# See more config options https://github.com/foundry-rs/foundry/tree/master/crates/config
+via_ir = false