diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 3af3c404f..ee11d34d5 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -932,7 +932,26 @@ void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
 void SMTEncoder::endVisit(Identifier const& _identifier)
 {
 	if (auto decl = identifierToVariable(_identifier))
-		defineExpr(_identifier, currentValue(*decl));
+	{
+		if (decl->isConstant())
+		{
+			if (RationalNumberType const* rationalType = isConstant(_identifier))
+			{
+				if (rationalType->isNegative())
+					defineExpr(_identifier, smtutil::Expression(u2s(rationalType->literalValue(nullptr))));
+				else
+					defineExpr(_identifier, smtutil::Expression(rationalType->literalValue(nullptr)));
+			}
+			else
+			{
+				solAssert(decl->value(), "");
+				decl->value()->accept(*this);
+				defineExpr(_identifier, expr(*decl->value()));
+			}
+		}
+		else
+			defineExpr(_identifier, currentValue(*decl));
+	}
 	else if (_identifier.annotation().type->category() == Type::Category::Function)
 		visitFunctionIdentifier(_identifier);
 	else if (_identifier.name() == "now")
diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_constant_bound.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_constant_bound.sol
new file mode 100644
index 000000000..d084fab5d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/overflow/overflow_constant_bound.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract DepositContract {
+    uint constant MAX_DEPOSIT_COUNT = 2**32 - 1;
+
+    uint256 deposit_count;
+    uint256 deposit_count_2;
+
+    function deposit() external {
+        require(deposit_count < MAX_DEPOSIT_COUNT);
+        deposit_count += 1;
+        deposit_count_2 += 10; // should fail
+    }
+}
+// ----
+// Warning 4984: (289-310): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 2661: (289-310): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.