diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 0af171a74..5b7807f7e 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -36,6 +36,15 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _
 	m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses)),
 	m_errorReporter(_errorReporter)
 {
+#if defined (HAVE_Z3) || defined (HAVE_CVC4)
+	if (!_smtlib2Responses.empty())
+		m_errorReporter.warning(
+			"SMT-LIB2 query responses were given in the auxiliary input, "
+			"but this Solidity binary uses an SMT solver (Z3/CVC4) directly."
+			"These responses will be ignored."
+			"Consider disabling Z3/CVC4 at compilation time in order to use SMT-LIB2 responses."
+		);
+#endif
 }
 
 void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp
index 2c95c3fa3..6bdbd3108 100644
--- a/libsolidity/formal/SMTPortfolio.cpp
+++ b/libsolidity/formal/SMTPortfolio.cpp
@@ -42,14 +42,6 @@ SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
 #endif
 #if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
 	m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses));
-#else
-	if (!_smtlib2Responses.empty())
-		m_errorReporter.warning(
-			"SMT-LIB2 query responses were given in the auxiliary input, "
-			"but this Solidity binary uses an SMT solver (Z3/CVC4) directly."
-			"These responses will be ignored."
-			"Consider disabling Z3/CVC4 at compilation time in order to use SMT-LIB2 responses."
-		);
 #endif
 	(void)_smtlib2Responses;
 }