diff --git a/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol b/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol
new file mode 100644
index 000000000..1b77598d8
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol
@@ -0,0 +1,43 @@
+pragma experimental SMTChecker;
+
+/**
+ * @title MerkleProof
+ * @dev Merkle proof verification based on
+ * https://github.com/ameensol/merkle-tree-solidity/blob/master/src/MerkleProof.sol
+ */
+library MerkleProof {
+    /**
+     * @dev Verifies a Merkle proof proving the existence of a leaf in a Merkle tree. Assumes that each pair of leaves
+     * and each pair of pre-images are sorted.
+     * @param proof Merkle proof containing sibling hashes on the branch from the leaf to the root of the Merkle tree
+     * @param root Merkle root
+     * @param leaf Leaf of Merkle tree
+     */
+    function verify(bytes32[] memory proof, bytes32 root, bytes32 leaf) internal pure returns (bool) {
+        bytes32 computedHash = leaf;
+
+        for (uint256 i = 0; i < proof.length; i++) {
+            bytes32 proofElement = proof[i];
+
+            if (computedHash < proofElement) {
+                // Hash(current computed hash + current element of the proof)
+                computedHash = keccak256(abi.encodePacked(computedHash, proofElement));
+            } else {
+                // Hash(current element of the proof + current computed hash)
+                computedHash = keccak256(abi.encodePacked(proofElement, computedHash));
+            }
+        }
+
+        // Check if the computed hash (root) is equal to the provided root
+        return computedHash == root;
+    }
+}
+
+// ----
+// Warning: (755-767): Assertion checker does not yet support this expression.
+// Warning: (988-1032): Assertion checker does not yet implement this type of function call.
+// Warning: (988-1032): Internal error: Expression undefined for SMT solver.
+// Warning: (1175-1219): Assertion checker does not yet implement this type of function call.
+// Warning: (1175-1219): Internal error: Expression undefined for SMT solver.
+// Warning: (755-767): Assertion checker does not yet support this expression.
+// Warning: (769-772): Overflow (resulting value larger than 2**256 - 1) happens here