diff --git a/packages/contracts/foundry.toml b/packages/contracts/foundry.toml
index 52d544eea..942a9be76 100644
--- a/packages/contracts/foundry.toml
+++ b/packages/contracts/foundry.toml
@@ -21,11 +21,11 @@ force = false
 mainnet = "https://rpc.ankr.com/eth"
 
 [profile.SMT.model_checker]
-contracts = { }
+contracts = { "test/formal/diamond/facets/UbiquityPoolFacetSMT.t.sol" = ["UbiquityPoolFacetSMT"]}
 engine = 'chc'
 solvers = ['z3']
 show_unproved = true
-timeout = 0
+timeout = 5000
 targets = [
   'assert',
   'constantCondition',
@@ -45,4 +45,4 @@ runs = 16500000   # 5h 30m
 max_test_rejects = 144000000
 
 [profile.intense.invariant]
-runs = 350000     # 5h 40m
\ No newline at end of file
+runs = 350000     # 5h 40m
diff --git a/packages/contracts/test/formal/diamond/facets/UbiquityPoolFacet.formal.t.sol b/packages/contracts/test/formal/diamond/facets/UbiquityPoolFacetSMT.t.sol
similarity index 81%
rename from packages/contracts/test/formal/diamond/facets/UbiquityPoolFacet.formal.t.sol
rename to packages/contracts/test/formal/diamond/facets/UbiquityPoolFacetSMT.t.sol
index e312bd793..849d95239 100644
--- a/packages/contracts/test/formal/diamond/facets/UbiquityPoolFacet.formal.t.sol
+++ b/packages/contracts/test/formal/diamond/facets/UbiquityPoolFacetSMT.t.sol
@@ -12,7 +12,7 @@ import {MockCurveStableSwapNG} from "../../../../src/dollar/mocks/MockCurveStabl
 import {MockCurveTwocryptoOptimized} from "../../../../src/dollar/mocks/MockCurveTwocryptoOptimized.sol";
 import {SafeMath} from "@openzeppelin/contracts/utils/math/SafeMath.sol";
 
-contract UbiquityPoolFacetFormalTest is DiamondTestSetup {
+contract UbiquityPoolFacetSMT is DiamondTestSetup {
     using SafeMath for uint256;
 
     // mock three tokens: collateral token, stable token, wrapped ETH token
@@ -147,23 +147,42 @@ contract UbiquityPoolFacetFormalTest is DiamondTestSetup {
         // user approves the pool to transfer collateral
         vm.prank(user);
         collateralToken.approve(address(ubiquityPoolFacet), 100e18);
+
+        vm.prank(user);
+        ubiquityPoolFacet.mintDollar(0, 1e18, 0.9e18, 1e18, 0, true);
     }
 
-    function testInitialCollateralSetup() public {
-        LibUbiquityPool.CollateralInformation
-            memory collateralInformation = ubiquityPoolFacet
-                .collateralInformation(address(collateralToken));
+    function testCannotMintMoreDollarsThanCollateral() public view {
+        (
+            uint256 totalDollarSupplyInUsd,
+            uint256 collateralUsdBalance
+        ) = getDollarSupplyAndCollateralBalance();
+        assert(totalDollarSupplyInUsd <= collateralUsdBalance);
+    }
 
-        assertTrue(
-            collateralInformation.isEnabled,
-            "Collateral token should be enabled initially"
-        );
+    function testCannotRedeemMoreCollateralThanDollarValue() public view {
+        (
+            uint256 totalDollarSupplyInUsd,
+            uint256 collateralUsdBalance
+        ) = getDollarSupplyAndCollateralBalance();
+        assert(collateralUsdBalance >= totalDollarSupplyInUsd);
+    }
 
-        uint256 expectedCeiling = 50_000e18; // Pool ceiling defined in setUp
-        assertEq(
-            collateralInformation.poolCeiling,
-            expectedCeiling,
-            "Collateral ceiling should be 50,000 tokens"
-        );
+    function getDollarSupplyAndCollateralBalance()
+        public
+        view
+        returns (uint256 totalDollarSupplyInUsd, uint256 collateralUsdBalance)
+    {
+        uint256 totalDollarSupply = IERC20Ubiquity(
+            managerFacet.dollarTokenAddress()
+        ).totalSupply();
+
+        collateralUsdBalance = ubiquityPoolFacet.collateralUsdBalance();
+
+        require(collateralUsdBalance > 0, "Collateral balance is zero");
+        require(totalDollarSupply > 0, "Dollar supply is zero");
+
+        uint256 dollarPrice = ubiquityPoolFacet.getDollarPriceUsd();
+        totalDollarSupplyInUsd = totalDollarSupply.mul(dollarPrice).div(1e6);
     }
 }