Merge pull request #15205 from pgebal/smtchecker/fix-show-proved-safe

SMTChecker: Fix internal compiler error on reporting proved targets
ethereum · Jun 21, 2024 · 3c65632 · 3c65632
2 parents 7711a8e + 6ccb3a3
commit 3c65632
Show file tree

Hide file tree

Showing 34 changed files with 94 additions and 34 deletions.
diff --git a/Changelog.md b/Changelog.md
@@ -12,7 +12,8 @@ Compiler Features:
 
 
 Bugfixes:
- * SMTChecker: Fix error that reports invalid number of verified checks for BMC engine.
+ * SMTChecker: Fix error that reports invalid number of verified checks for BMC and CHC engines.
+ * SMTChecker: Fix internal compiler error when reporting proved targets 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
@@ -47,12 +47,13 @@ BMC::BMC(
 	smt::EncodingContext& _context,
 	UniqueErrorReporter& _errorReporter,
 	UniqueErrorReporter& _unsupportedErrorReporter,
+	ErrorReporter& _provedSafeReporter,
 	std::map<h256, std::string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
 	ModelCheckerSettings _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider)
+	SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _provedSafeReporter, _charStreamProvider)
 {
 	solAssert(!_settings.printQuery || _settings.solvers == SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries");
 	std::vector<std::unique_ptr<SolverInterface>> solvers;
@@ -133,15 +134,14 @@ void BMC::analyze(SourceUnit const& _source, std::map<ASTNode const*, std::set<V
 	else if (m_settings.showProvedSafe)
 		for (auto const& [node, targets]: m_safeTargets)
 			for (auto const& target: targets)
-				m_errorReporter.info(
+				m_provedSafeReporter.info(
 					2961_error,
 					node->location(),
 					"BMC: " +
 					targetDescription(target) +
 					" check is safe!"
 				);
 
-
 	// If this check is true, Z3 and cvc5 are not available
 	// and the query answers were not provided, since SMTPortfolio
 	// guarantees that SmtLib2Interface is the first solver, if enabled.

diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h
@@ -62,6 +62,7 @@ class BMC: public SMTEncoder
 		smt::EncodingContext& _context,
 		langutil::UniqueErrorReporter& _errorReporter,
 		langutil::UniqueErrorReporter& _unsupportedErrorReporter,
+		langutil::ErrorReporter& _provedSafeReporter,
 		std::map<h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		ModelCheckerSettings _settings,

diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
@@ -63,12 +63,13 @@ CHC::CHC(
 	EncodingContext& _context,
 	UniqueErrorReporter& _errorReporter,
 	UniqueErrorReporter& _unsupportedErrorReporter,
+	ErrorReporter& _provedSafeReporter,
 	std::map<util::h256, std::string> const& _smtlib2Responses,
 	ReadCallback::Callback const& _smtCallback,
 	ModelCheckerSettings _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider),
+	SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _provedSafeReporter, _charStreamProvider),
 	m_smtlib2Responses(_smtlib2Responses),
 	m_smtCallback(_smtCallback)
 {
@@ -2116,17 +2117,22 @@ void CHC::checkVerificationTargets()
 		);
 
 	if (!m_settings.showProvedSafe && !m_safeTargets.empty())
+	{
+		std::size_t provedSafeNum = 0;
+		for (auto&& [_, targets]: m_safeTargets)
+			provedSafeNum += targets.size();
 		m_errorReporter.info(
 			1391_error,
 			"CHC: " +
-			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)
-				m_errorReporter.info(
+				m_provedSafeReporter.info(
 					9576_error,
 					node->location(),
 					"CHC: " +

diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h
@@ -58,6 +58,7 @@ class CHC: public SMTEncoder
 		smt::EncodingContext& _context,
 		langutil::UniqueErrorReporter& _errorReporter,
 		langutil::UniqueErrorReporter& _unsupportedErrorReporter,
+		langutil::ErrorReporter& _provedSafeReporter,
 		std::map<util::h256, std::string> const& _smtlib2Responses,
 		ReadCallback::Callback const& _smtCallback,
 		ModelCheckerSettings _settings,
@@ -77,14 +78,25 @@ class CHC: public SMTEncoder
 		}
 	};
 
+	struct SafeTargetsCompare
+	{
+		bool operator()(CHCVerificationTarget const & _lhs, CHCVerificationTarget const & _rhs) const
+		{
+			if (_lhs.errorNode->id() == _rhs.errorNode->id())
+				return _lhs.type  < _rhs.type;
+			else
+				return _lhs.errorNode->id() == _rhs.errorNode->id();
+		}
+	};
+
 	struct ReportTargetInfo
 	{
 		langutil::ErrorId error;
 		langutil::SourceLocation location;
 		std::string message;
 	};
 
-	std::map<ASTNode const*, std::set<CHCVerificationTarget>, smt::EncodingContext::IdCompare> const& safeTargets() const { return m_safeTargets; }
+	std::map<ASTNode const*, std::set<CHCVerificationTarget, SafeTargetsCompare>, smt::EncodingContext::IdCompare> const& safeTargets() const { return m_safeTargets; }
 	std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> const& unsafeTargets() const { return m_unsafeTargets; }
 
 	/// This is used if the Horn solver is not directly linked into this binary.
@@ -423,7 +435,7 @@ class CHC: public SMTEncoder
 	std::map<unsigned, CHCVerificationTarget> m_verificationTargets;
 
 	/// Targets proved safe.
-	std::map<ASTNode const*, std::set<CHCVerificationTarget>, smt::EncodingContext::IdCompare> m_safeTargets;
+	std::map<ASTNode const*, std::set<CHCVerificationTarget, SafeTargetsCompare>, smt::EncodingContext::IdCompare> m_safeTargets;
 	/// Targets proved unsafe.
 	std::map<ASTNode const*, std::map<VerificationTargetType, ReportTargetInfo>, smt::EncodingContext::IdCompare> m_unsafeTargets;
 	/// Targets not proved.

diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp
@@ -43,10 +43,11 @@ ModelChecker::ModelChecker(
 	ReadCallback::Callback const& _smtCallback
 ):
 	m_errorReporter(_errorReporter),
+	m_provedSafeReporter(m_provedSafeLogs),
 	m_settings(std::move(_settings)),
 	m_context(),
-	m_bmc(m_context, m_uniqueErrorReporter, m_unsupportedErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
-	m_chc(m_context, m_uniqueErrorReporter, m_unsupportedErrorReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
+	m_bmc(m_context, m_uniqueErrorReporter, m_unsupportedErrorReporter, m_provedSafeReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider),
+	m_chc(m_context, m_uniqueErrorReporter, m_unsupportedErrorReporter, m_provedSafeReporter, _smtlib2Responses, _smtCallback, m_settings, _charStreamProvider)
 {
 }
 
@@ -151,6 +152,12 @@ void ModelChecker::analyze(SourceUnit const& _source)
 
 	m_errorReporter.append(m_uniqueErrorReporter.errors());
 	m_uniqueErrorReporter.clear();
+
+	if (m_settings.showProvedSafe)
+	{
+		m_errorReporter.append(m_provedSafeReporter.errors());
+		m_provedSafeReporter.clear();
+	}
 }
 
 std::vector<std::string> ModelChecker::unhandledQueries()

diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h
@@ -95,6 +95,12 @@ class ModelChecker
 	/// to m_errorReporter at the end of the analysis.
 	langutil::UniqueErrorReporter m_unsupportedErrorReporter;
 
+	langutil::ErrorList m_provedSafeLogs;
+	/// Used by SMTEncoder, BMC and CHC to accumulate info about proved targets.
+	/// This is local to ModelChecker, so needs to be appended
+	/// to m_errorReporter at the end of the analysis.
+	langutil::ErrorReporter m_provedSafeReporter;
+
 	ModelCheckerSettings m_settings;
 
 	/// Stores the context of the encoding.

diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
@@ -51,10 +51,12 @@ SMTEncoder::SMTEncoder(
 	ModelCheckerSettings _settings,
 	UniqueErrorReporter& _errorReporter,
 	UniqueErrorReporter& _unsupportedErrorReporter,
+	ErrorReporter& _provedSafeReporter,
 	langutil::CharStreamProvider const& _charStreamProvider
 ):
 	m_errorReporter(_errorReporter),
 	m_unsupportedErrors(_unsupportedErrorReporter),
+	m_provedSafeReporter(_provedSafeReporter),
 	m_context(_context),
 	m_settings(std::move(_settings)),
 	m_charStreamProvider(_charStreamProvider)

diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
@@ -57,6 +57,7 @@ class SMTEncoder: public ASTConstVisitor
 		ModelCheckerSettings _settings,
 		langutil::UniqueErrorReporter& _errorReporter,
 		langutil::UniqueErrorReporter& _unsupportedErrorReporter,
+		langutil::ErrorReporter& _provedSafeReporter,
 		langutil::CharStreamProvider const& _charStreamProvider
 	);
 
@@ -463,6 +464,7 @@ class SMTEncoder: public ASTConstVisitor
 
 	langutil::UniqueErrorReporter& m_errorReporter;
 	langutil::UniqueErrorReporter& m_unsupportedErrors;
+	langutil::ErrorReporter& m_provedSafeReporter;
 
 	/// Stores the current function/modifier call/invocation path.
 	std::vector<CallStackEntry> m_callStack;

diff --git a/scripts/error_codes.py b/scripts/error_codes.py
@@ -205,7 +205,6 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
         "7053", # Unimplemented feature error (parsing stage), currently has no tests
         "1180", # SMTChecker, covered by CL tests
         "2339", # SMTChecker, covered by CL tests
-        "2961", # SMTChecker, covered by CL tests
         "6240", # SMTChecker, covered by CL tests
     }
     assert len(test_ids & white_ids) == 0, "The sets are not supposed to intersect"

diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_compound_assignment.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_compound_assignment.sol
@@ -13,4 +13,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (128-145): CHC: Assertion violation happens here.
-// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/...ity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init.sol b/...ity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init.sol
@@ -39,4 +39,4 @@ contract C is B {
 // Warning 6328: (389-412): CHC: Assertion violation happens here.
 // Warning 6328: (489-513): CHC: Assertion violation happens here.
 // Warning 6328: (533-546): CHC: Assertion violation happens here.
-// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 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/inheritance/constructor_state_variable_init_asserts.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_asserts.sol
@@ -37,4 +37,4 @@ contract C is B {
 // Warning 6328: (339-362): CHC: Assertion violation happens here.
 // Warning 6328: (439-463): CHC: Assertion violation happens here.
 // Warning 6328: (483-496): CHC: Assertion violation happens here.
-// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 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/inheritance/constructor_state_variable_init_chain_tree.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_tree.sol
@@ -41,4 +41,4 @@ contract C is B {
 // ----
 // Warning 6328: (403-417): CHC: Assertion violation happens here.
 // Warning 6328: (450-463): CHC: Assertion violation happens here.
-// Info 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 8 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol b/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol
@@ -34,4 +34,4 @@ contract E is C,D {
 // SMTIgnoreCex: no
 // ----
 // Warning 6328: (379-394): CHC: Assertion violation happens here.\nCounterexample:\nx = 111\n\nTransaction trace:\nE.constructor()\nState: x = 0\nE.f()\n    C.f() -- internal call\n        B.f() -- internal call\n            A.f() -- internal call
-// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 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/assignment_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol
@@ -30,4 +30,4 @@ contract A {
 // SMTIgnoreInv: yes
 // ----
 // Warning 6328: (392-408): CHC: Assertion violation happens here.
-// Info 1391: CHC: 17 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 26 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/assignment_module_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol
@@ -31,4 +31,4 @@ contract A {
 // ----
 // Warning 6328: (AASource:159-178): CHC: Assertion violation happens here.
 // Warning 6328: (AASource:370-386): CHC: Assertion violation happens here.
-// Info 1391: CHC: 16 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 25 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/division_4.sol b/test/libsolidity/smtCheckerTests/operators/division_4.sol
@@ -8,4 +8,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 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/division_truncates_correctly_2.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_2.sol
@@ -8,4 +8,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 3 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/division_truncates_correctly_3.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_3.sol
@@ -8,4 +8,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 3 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/division_truncates_correctly_4.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_4.sol
@@ -8,4 +8,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 3 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/division_truncates_correctly_5.sol b/test/libsolidity/smtCheckerTests/operators/division_truncates_correctly_5.sol
@@ -8,4 +8,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 3 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/mod.sol b/test/libsolidity/smtCheckerTests/operators/mod.sol
@@ -10,4 +10,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 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/mod_signed.sol b/test/libsolidity/smtCheckerTests/operators/mod_signed.sol
@@ -12,5 +12,5 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (131-148): CHC: Assertion violation might happen here.
-// Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
 // Info 6002: BMC: 1 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_add_array_push_2.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_array_push_2.sol
@@ -18,4 +18,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Info 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 8 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_chc.sol b/test/libsolidity/smtCheckerTests/operators/unary_minus_chc.sol
@@ -8,4 +8,4 @@ contract C
 // SMTEngine: chc
 // ----
 //  Warning 6328: (48-63): CHC: Assertion violation happens here.
-//  Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+//  Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/...ibsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants.sol b/...ibsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants.sol
@@ -60,4 +60,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Info 1391: CHC: 22 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 27 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/...idity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants_fail.sol b/...idity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants_fail.sol
@@ -76,4 +76,4 @@ contract C {
 // Warning 6328: (2741-2758): CHC: Assertion violation happens here.
 // Warning 6328: (2783-2804): CHC: Assertion violation happens here.
 // Warning 6328: (2829-2850): CHC: Assertion violation happens here.
-// Info 1391: CHC: 6 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 11 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_show_proved.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_and_underflow_bmc_show_proved.sol
@@ -0,0 +1,13 @@
+contract C {
+	function f(int x, int y) public pure returns (int) {
+		require(x == 0);
+		require(y == 0);
+		return x + y;
+	}
+}
+// ====
+// SMTEngine: bmc
+// SMTShowProvedSafe: yes
+// ----
+// Info 2961: (114-119): BMC: Underflow (resulting value less than -2**255) check is safe!
+// Info 2961: (114-119): BMC: Overflow (resulting value larger than 2**255 - 1) check is safe!
diff --git a/test/libsolidity/smtCheckerTests/overflow/overflow_and_underflow_chc.sol b/test/libsolidity/smtCheckerTests/overflow/overflow_and_underflow_chc.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: chc
+// ----
+// Info 1391: CHC: 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/overflow/signed_guard_sum_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_guard_sum_overflow.sol
@@ -10,4 +10,4 @@ contract C  {
 // ----
 // Warning 3944: (78-83): CHC: Underflow (resulting value less than -2**255) happens here.
 // Warning 4984: (78-83): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.
-// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 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/try_catch/try_3.sol b/test/libsolidity/smtCheckerTests/try_catch/try_3.sol
@@ -25,4 +25,4 @@ contract C {
 // ----
 // Warning 5667: (259-273): Unused try/catch parameter. Remove or comment out the variable name to silence this warning.
 // Warning 6328: (280-294): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\ns = []\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n    C.postinc() -- internal call
-// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/typecast/downcast.sol b/test/libsolidity/smtCheckerTests/typecast/downcast.sol
@@ -46,4 +46,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Info 1391: CHC: 20 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 24 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/unchecked/flipping_sign_tests.sol b/test/libsolidity/smtCheckerTests/unchecked/flipping_sign_tests.sol
@@ -11,4 +11,4 @@ contract test {
 // ----
 // Warning 4984: (117-119): CHC: Overflow (resulting value larger than 2**255 - 1) happens here.
 // Warning 6328: (110-125): CHC: Assertion violation happens here.
-// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.