From 54bed454f6e7a53f51ec7e9bda7805900a2c8472 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Fri, 13 Oct 2017 17:57:58 +0200
Subject: Rename function and warn if responses are supplied for Z3.

---
 libsolidity/formal/SMTPortfolio.cpp | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'libsolidity/formal')

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;
 }
-- 
cgit