diff --git a/tests/expected/all.json b/tests/expected/all.json
index 43419621..225f9682 100644
--- a/tests/expected/all.json
+++ b/tests/expected/all.json
@@ -778,6 +778,24 @@
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
+            },
+            {
+                "name": "check_deposit(uint256,uint256,uint256)",
+                "exitcode": 1,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_mint(uint256,uint256,uint256)",
+                "exitcode": 1,
+                "num_models": 1,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
             }
         ],
         "test/Natspec.t.sol:NatspecTestContract": [
diff --git a/tests/foundry.toml b/tests/foundry.toml
index 0f874219..269e20b6 100644
--- a/tests/foundry.toml
+++ b/tests/foundry.toml
@@ -6,3 +6,5 @@ libs = ['lib']
 # See more config options https://github.com/foundry-rs/foundry/tree/master/config
 force = false
 evm_version = 'shanghai'
+
+extra_output = ["storageLayout", "metadata"]
diff --git a/tests/test/Math.t.sol b/tests/test/Math.t.sol
index e42286ed..5191a467 100644
--- a/tests/test/Math.t.sol
+++ b/tests/test/Math.t.sol
@@ -9,4 +9,45 @@ contract MathTest {
             assert(r1 == r2);
         }
     }
+
+    function _check_deposit(uint a, uint A1, uint S1) public pure returns (bool) {
+        uint s = (a * S1) / A1;
+
+        uint A2 = A1 + a;
+        uint S2 = S1 + s;
+
+        return (A1 / S1 <= A2 / S2); // always true
+    }
+
+    // NOTE: currently timeout when --smt-div is enabled; producing invalid counterexamples when --smt-div is not given
+    function check_deposit(uint a, uint A1, uint S1) public pure {
+        assert(_check_deposit(a, A1, S1)); // no counterexample
+    }
+
+    function test_deposit(uint a, uint A1, uint S1) public {
+        (bool success, bytes memory retdata) = address(this).call(abi.encodeWithSelector(this._check_deposit.selector, a, A1, S1));
+        if (!success) return;
+        assert(abi.decode(retdata, (bool)));
+    }
+
+    function _check_mint(uint s, uint A1, uint S1) public pure returns (bool) {
+        uint a = (s * A1) / S1;
+
+        uint A2 = A1 + a;
+        uint S2 = S1 + s;
+
+        // (A1 / S1 <= A2 / S2)
+        return (A1 * S2 <= A2 * S1); // can be false
+    }
+
+    /// @custom:halmos --smt-div
+    function check_mint(uint s, uint A1, uint S1) public pure {
+        assert(_check_mint(s, A1, S1)); // counterexamples exist
+    }
+
+    function test_mint(uint s, uint A1, uint S1) public {
+        (bool success, bytes memory retdata) = address(this).call(abi.encodeWithSelector(this._check_mint.selector, s, A1, S1));
+        if (!success) return;
+        assert(abi.decode(retdata, (bool)));
+    }
 }