From f3c2309c736ffcdb84fc133106b05d1be1eda95a Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Fri, 3 Aug 2018 17:04:56 +0200
Subject: [PATCH] Display better error message in SMTLib2

---
 libsolidity/formal/SMTLib2Interface.cpp | 8 ++++----
 libsolidity/formal/SMTLib2Interface.h   | 4 ++--
 libsolidity/formal/SMTPortfolio.cpp     | 6 ++++--
 3 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 80ecc715d..3cfa01b19 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -39,8 +39,8 @@ using namespace dev;
 using namespace dev::solidity;
 using namespace dev::solidity::smt;
 
-SMTLib2Interface::SMTLib2Interface(map<h256, string> const& _smtlib2Responses):
-	m_smtlib2Responses(_smtlib2Responses)
+SMTLib2Interface::SMTLib2Interface(map<h256, string> const& _queryResponses):
+	m_queryResponses(_queryResponses)
 {
 	reset();
 }
@@ -215,8 +215,8 @@ vector<string> SMTLib2Interface::parseValues(string::const_iterator _start, stri
 string SMTLib2Interface::querySolver(string const& _input)
 {
 	h256 inputHash = dev::keccak256(_input);
-	if (m_smtlib2Responses.count(inputHash))
-		return m_smtlib2Responses.at(inputHash);
+	if (m_queryResponses.count(inputHash))
+		return m_queryResponses.at(inputHash);
 	else
 	{
 		m_unhandledQueries.push_back(_input);
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index c67101ae5..55fc4096d 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -44,7 +44,7 @@ namespace smt
 class SMTLib2Interface: public SolverInterface, public boost::noncopyable
 {
 public:
-	explicit SMTLib2Interface(std::map<h256, std::string> const& _smtlib2Responses);
+	explicit SMTLib2Interface(std::map<h256, std::string> const& _queryResponses);
 
 	void reset() override;
 
@@ -73,10 +73,10 @@ private:
 	/// Communicates with the solver via the callback. Throws SMTSolverError on error.
 	std::string querySolver(std::string const& _input);
 
-	std::map<h256, std::string> const& m_smtlib2Responses;
 	std::vector<std::string> m_accumulatedOutput;
 	std::set<std::string> m_variables;
 
+	std::map<h256, std::string> const& m_queryResponses;
 	std::vector<std::string> m_unhandledQueries;
 };
 
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp
index 515d6f32c..2c95c3fa3 100644
--- a/libsolidity/formal/SMTPortfolio.cpp
+++ b/libsolidity/formal/SMTPortfolio.cpp
@@ -45,8 +45,10 @@ SMTPortfolio::SMTPortfolio(map<h256, string> const& _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."
+			"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;