Check early if solvers are available.

libsolidity/formal/BMC.cpp

@@ -63,15 +63,14 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 {
 	if (m_interface->solvers() == 0)
 	{
-		if (!m_noSolverWarning)
-		{
-			m_noSolverWarning = true;
 		m_errorReporter.warning(
 			7710_error,
 			SourceLocation(),
 			"BMC analysis was not possible since no SMT solver was found and enabled."
+#ifdef HAVE_Z3_DLOPEN
+			" Install libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " to enable Z3."
+#endif
 		);
-		}
 		return;
 	}
 
@@ -108,10 +107,6 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 		m_interface->solvers() == 1 &&
 		m_settings.solvers.smtlib2
 	)
-	{
-		if (!m_noSolverWarning)
-		{
-			m_noSolverWarning = true;
 		m_errorReporter.warning(
 			8084_error,
 			SourceLocation(),
@@ -122,8 +117,6 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 #endif
 		);
 }
-	}
-}
 
 bool BMC::shouldInlineFunctionCall(
 	FunctionCall const& _funCall,

libsolidity/formal/CHC.cpp

@@ -60,21 +60,15 @@ using namespace solidity::frontend::smt;
 CHC::CHC(
 	EncodingContext& _context,
 	UniqueErrorReporter& _errorReporter,
-	[[maybe_unused]] map<util::h256, string> const& _smtlib2Responses,
+	map<util::h256, string> const& _smtlib2Responses,
-	[[maybe_unused]] ReadCallback::Callback const& _smtCallback,
+	ReadCallback::Callback const& _smtCallback,
 	ModelCheckerSettings const& _settings,
 	CharStreamProvider const& _charStreamProvider
 ):
-	SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider)
+	SMTEncoder(_context, _settings, _errorReporter, _charStreamProvider),
+	m_smtlib2Responses(_smtlib2Responses),
+	m_smtCallback(_smtCallback)
 {
-	bool usesZ3 = m_settings.solvers.z3;
-#ifdef HAVE_Z3
-	usesZ3 = usesZ3 && Z3Interface::available();
-#else
-	usesZ3 = false;
-#endif
-	if (!usesZ3 && m_settings.solvers.smtlib2)
-		m_interface = make_unique<CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback, m_settings.timeout);
 }
 
 void CHC::analyze(SourceUnit const& _source)
@@ -82,17 +76,26 @@ void CHC::analyze(SourceUnit const& _source)
 	if (!shouldAnalyze(_source))
 		return;
 
-	if (!m_settings.solvers.z3 && !m_settings.solvers.smtlib2)
+	bool usesZ3 = m_settings.solvers.z3;
+#ifdef HAVE_Z3_DLOPEN
+	if (m_settings.solvers.z3 && !Z3Interface::available())
 	{
-		if (!m_noSolverWarning)
+		usesZ3 = false;
+		m_errorReporter.warning(
+			8158_error,
+			SourceLocation(),
+			"z3 was selected as a Horn solver for CHC analysis but libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
+		);
+	}
+#endif
+
+	if (!usesZ3 && !m_settings.solvers.smtlib2)
 	{
-			m_noSolverWarning = true;
 		m_errorReporter.warning(
 			7649_error,
 			SourceLocation(),
-				"CHC analysis was not possible since no Horn solver was enabled."
+			"CHC analysis was not possible since no Horn solver was found and enabled."
 		);
-		}
 		return;
 	}
 
@@ -115,21 +118,14 @@ void CHC::analyze(SourceUnit const& _source)
 	// actually given and the queries were solved.
 	if (auto const* smtLibInterface = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
 		ranSolver = smtLibInterface->unhandledQueries().empty();
-	if (!ranSolver && !m_noSolverWarning)
+	if (!ranSolver)
-	{
-		m_noSolverWarning = true;
 		m_errorReporter.warning(
 			3996_error,
 			SourceLocation(),
-#ifdef HAVE_Z3_DLOPEN
-			"CHC analysis was not possible since libz3.so." + to_string(Z3_MAJOR_VERSION) + "." + to_string(Z3_MINOR_VERSION) + " was not found."
-#else
 			"CHC analysis was not possible. No Horn solver was available."
 			" None of the installed solvers was enabled."
-#endif
 		);
 }
-}
 
 vector<string> CHC::unhandledQueries() const
 {
@@ -1012,6 +1008,11 @@ void CHC::resetSourceAnalysis()
 #endif
 	if (!usesZ3)
 	{
+		solAssert(m_settings.solvers.smtlib2);
+
+		if (!m_interface)
+			m_interface = make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.timeout);
+
 		auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
 		solAssert(smtlib2Interface, "");
 		smtlib2Interface->reset();

libsolidity/formal/CHC.h

@@ -421,6 +421,9 @@ private:
 
 	/// CHC solver.
 	std::unique_ptr<smtutil::CHCSolverInterface> m_interface;
+
+	std::map<util::h256, std::string> const& m_smtlib2Responses;
+	ReadCallback::Callback const& m_smtCallback;
 };
 
 }

libsolidity/formal/SMTEncoder.h

@@ -426,8 +426,6 @@ protected:
 
 	smt::VariableUsage m_variableUsage;
 	bool m_arrayAssignmentHappened = false;
-	// True if the "No SMT solver available" warning was already created.
-	bool m_noSolverWarning = false;
 
 	/// Stores the instances of an Uninterpreted Function applied to arguments.
 	/// These may be direct application of UFs or Array index access.