Rename function and warn if responses are supplied for Z3.

3 files changed, 13 insertions, 7 deletions

diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp
index 4c591380..515d6f32 100644
--- a/libsolidity/formal/SMTPortfolio.cpp
+++ b/libsolidity/formal/SMTPortfolio.cpp
@@ -41,7 +41,13 @@ SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
 	m_solvers.emplace_back(make_shared<smt::CVC4Interface>());
 #endif
 #if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
-	m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses)),
+	m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses));
+#else
+	if (!_smtlib2Responses.empty())
+		m_errorReporter.warning(
+			"Query responses for smtlib2 were given in the auxiliary input, "
+			"but this Solidity binary uses an SMT solver directly."
+		);
 #endif
 	(void)_smtlib2Responses;
 }
diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h
index 3fceed24..2c7add3b 100644
--- a/libsolidity/interface/CompilerStack.h
+++ b/libsolidity/interface/CompilerStack.h
@@ -156,10 +156,6 @@ public:
 	/// Adds a response to an SMTLib2 query (identified by the hash of the query input).
 	void addSMTLib2Response(h256 const& _hash, std::string const& _response) { m_smtlib2Responses[_hash] = _response; }
 
-	/// @returns a list of unhandled queries to the SMT solver (has to be supplied in a second run
-	/// by calling @a addSMTLib2Response.
-	std::vector<std::string> const& unhandledSMTQueries() const { return m_unhandledSMTLib2Queries; }
-
 	/// Parses all source units that were added
 	/// @returns false on error.
 	bool parse();
@@ -195,6 +191,10 @@ public:
 	/// start line, start column, end line, end column
 	std::tuple<int, int, int, int> positionFromSourceLocation(langutil::SourceLocation const& _sourceLocation) const;
 
+	/// @returns a list of unhandled queries to the SMT solver (has to be supplied in a second run
+	/// by calling @a addSMTLib2Response).
+	std::vector<std::string> const& unhandledSMTLib2Queries() const { return m_unhandledSMTLib2Queries; }
+
 	/// @returns a list of the contract names in the sources.
 	std::vector<std::string> contractNames() const;
 
diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp
index 59c28cd9..a3cb90b1 100644
--- a/libsolidity/interface/StandardCompiler.cpp
+++ b/libsolidity/interface/StandardCompiler.cpp
@@ -539,8 +539,8 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
 	if (errors.size() > 0)
 		output["errors"] = errors;
 
-	if (!m_compilerStack.unhandledSMTQueries().empty())
-		for (string const& query: m_compilerStack.unhandledSMTQueries())
+	if (!m_compilerStack.unhandledSMTLib2Queries().empty())
+		for (string const& query: m_compilerStack.unhandledSMTLib2Queries())
 			output["auxiliaryInputRequested"]["smtlib2"]["0x" + keccak256(query).hex()] = query;
 
 	output["sources"] = Json::objectValue;