diff --git a/Changelog.md b/Changelog.md
index 29fb86250b6e..de3fc3d6cf13 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -11,6 +11,7 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Fix error that reports invalid number of verified checks for BMC engine.
  * TypeChecker: Fix segfault when assigning nested tuple to tuple.
  * Yul Optimizer: Name simplification could lead to forbidden identifiers with a leading and/or trailing dot, e.g., ``x._`` would get simplified into ``x.``.
 
diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index 916bf5a31db0..b1a326fc77c4 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -118,13 +118,18 @@ void BMC::analyze(SourceUnit const& _source, std::map<ASTNode const*, std::set<V
 		);
 
 	if (!m_settings.showProvedSafe && !m_safeTargets.empty())
+	{
+		std::size_t provedSafeNum = 0;
+		for (auto&& [_, targets]: m_safeTargets)
+			provedSafeNum += targets.size();
 		m_errorReporter.info(
 			6002_error,
 			"BMC: " +
-			std::to_string(m_safeTargets.size()) +
+			std::to_string(provedSafeNum) +
 			" verification condition(s) proved safe!" +
 			" Enable the model checker option \"show proved safe\" to see all of them."
 		);
+	}
 	else if (m_settings.showProvedSafe)
 		for (auto const& [node, targets]: m_safeTargets)
 			for (auto const& target: targets)
diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h
index 1f97cbeef480..5ed61b839981 100644
--- a/libsolidity/formal/BMC.h
+++ b/libsolidity/formal/BMC.h
@@ -149,7 +149,10 @@ class BMC: public SMTEncoder
 
 		friend bool operator<(BMCVerificationTarget const& _a, BMCVerificationTarget const& _b)
 		{
-			return _a.expression->id() < _b.expression->id();
+			if (_a.expression->id() == _b.expression->id())
+				return _a.type < _b.type;
+			else
+				return _a.expression->id() < _b.expression->id();
 		}
 	};
 
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init.sol
index 4728a1cb0e61..a5ec4d87f539 100644
--- a/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init.sol
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init.sol
@@ -39,4 +39,4 @@ contract C is B {
 // Warning 4661: (389-412): BMC: Assertion violation happens here.
 // Warning 4661: (489-513): BMC: Assertion violation happens here.
 // Warning 4661: (533-546): BMC: Assertion violation happens here.
-// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 6002: BMC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/operators/unary_minus_bmc.sol b/test/libsolidity/smtCheckerTests/operators/unary_minus_bmc.sol
index 052554d21c63..66e80539d097 100644
--- a/test/libsolidity/smtCheckerTests/operators/unary_minus_bmc.sol
+++ b/test/libsolidity/smtCheckerTests/operators/unary_minus_bmc.sol
@@ -8,4 +8,4 @@ contract C
 // SMTEngine: bmc
 // ----
 // Warning 4661: (48-63): BMC: Assertion violation happens here.
-// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 6002: BMC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol
index 33665ee26dcc..9872a6a92b26 100644
--- a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol
+++ b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol
@@ -77,4 +77,4 @@ contract C {
 // Warning 4144: (953-982): BMC: Underflow (resulting value less than -32768) happens here.
 // Warning 3046: (1149-1178): BMC: Division by zero happens here.
 // Warning 7812: (2245-2271): BMC: Assertion violation might happen here.
-// Info 6002: BMC: 8 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 6002: BMC: 10 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_and_underflow_bmc.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_and_underflow_bmc.sol
new file mode 100644
index 000000000000..b788acebf3a5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/overflow/overflow_and_underflow_bmc.sol
@@ -0,0 +1,11 @@
+contract C {
+	function f(int x, int y) public pure returns (int) {
+		require(x == 0);
+		require(y == 0);
+		return x + y;
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Info 6002: BMC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.