Merge pull request #3073 from ethereum/smtlib2_via_standardio

Inject SMTLIB2 queries and responses via standard-json-io.

24 files changed, 356 insertions, 26 deletions

diff --git a/Changelog.md b/Changelog.md
index 449798a4..ca904ffc 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -6,6 +6,7 @@ Language Features:
 Compiler Features:
  * Build System: LLL is not built anymore by default. Must configure it with CMake as `-DLLL=ON`.
  * Code generator: Do not perform redundant double cleanup on unsigned integers when loading from calldata.
+ * SMTChecker: SMTLib2 queries and responses passed via standard JSON compiler interface.
  * SMTChecker: Support ``msg``, ``tx`` and ``block`` member variables.
  * SMTChecker: Support ``gasleft()`` and ``blockhash()`` functions.
  * SMTChecker: Support internal bound function calls.
diff --git a/libdevcore/JSON.cpp b/libdevcore/JSON.cpp
index 6317cc89..086fae50 100644
--- a/libdevcore/JSON.cpp
+++ b/libdevcore/JSON.cpp
@@ -21,6 +21,8 @@
 
 #include "JSON.h"
 
+#include "CommonIO.h"
+
 #include <sstream>
 #include <map>
 #include <memory>
@@ -111,4 +113,10 @@ bool jsonParse(string const& _input, Json::Value& _json, string *_errs /* = null
 	return parse(readerBuilder, _input, _json, _errs);
 }
 
+bool jsonParseFile(string const& _fileName, Json::Value& _json, string *_errs /* = nullptr */)
+{
+	return jsonParse(readFileAsString(_fileName), _json, _errs);
+}
+
+
 } // namespace dev
diff --git a/libdevcore/JSON.h b/libdevcore/JSON.h
index 1ce822cd..ecb93467 100644
--- a/libdevcore/JSON.h
+++ b/libdevcore/JSON.h
@@ -48,4 +48,11 @@ bool jsonParseStrict(std::string const& _input, Json::Value& _json, std::string*
 /// \return \c true if the document was successfully parsed, \c false if an error occurred.
 bool jsonParse(std::string const& _input, Json::Value& _json, std::string* _errs = nullptr);
 
+/// Parse a JSON string (@a _input) and writes resulting JSON object to (@a _json)
+/// \param _input file containing JSON input
+/// \param _json [out] resulting JSON object
+/// \param _errs [out] Formatted error messages
+/// \return \c true if the document was successfully parsed, \c false if an error occurred.
+bool jsonParseFile(std::string const& _fileName, Json::Value& _json, std::string* _errs = nullptr);
+
 }
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index bb9b498f..5b7807f7 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -32,10 +32,19 @@ using namespace dev;
 using namespace langutil;
 using namespace dev::solidity;
 
-SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback):
-	m_interface(make_shared<smt::SMTPortfolio>(_readFileCallback)),
+SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
+	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/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 5f51beb7..34724848 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -47,10 +47,15 @@ class VariableUsage;
 class SMTChecker: private ASTConstVisitor
 {
 public:
-	SMTChecker(langutil::ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback);
+	SMTChecker(langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
 
 	void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner);
 
+	/// This is used if the SMT solver is not directly linked into this binary.
+	/// @returns a list of inputs to the SMT solver that were not part of the argument to
+	/// the constructor.
+	std::vector<std::string> unhandledQueries() { return m_interface->unhandledQueries(); }
+
 private:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
 	// because the order of expression evaluation is undefined
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 55c72cfc..3cfa01b1 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -20,6 +20,8 @@
 #include <liblangutil/Exceptions.h>
 #include <libsolidity/interface/ReadFile.h>
 
+#include <libdevcore/Keccak256.h>
+
 #include <boost/algorithm/string/predicate.hpp>
 #include <boost/algorithm/string/join.hpp>
 #include <boost/filesystem/operations.hpp>
@@ -37,8 +39,8 @@ using namespace dev;
 using namespace dev::solidity;
 using namespace dev::solidity::smt;
 
-SMTLib2Interface::SMTLib2Interface(ReadCallback::Callback const& _queryCallback):
-	m_queryCallback(_queryCallback)
+SMTLib2Interface::SMTLib2Interface(map<h256, string> const& _queryResponses):
+	m_queryResponses(_queryResponses)
 {
 	reset();
 }
@@ -212,11 +214,12 @@ vector<string> SMTLib2Interface::parseValues(string::const_iterator _start, stri
 
 string SMTLib2Interface::querySolver(string const& _input)
 {
-	if (!m_queryCallback)
-		BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment("No SMT solver available."));
-
-	ReadCallback::Result queryResult = m_queryCallback(_input);
-	if (!queryResult.success)
-		BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment(queryResult.responseOrErrorMessage));
-	return queryResult.responseOrErrorMessage;
+	h256 inputHash = dev::keccak256(_input);
+	if (m_queryResponses.count(inputHash))
+		return m_queryResponses.at(inputHash);
+	else
+	{
+		m_unhandledQueries.push_back(_input);
+		return "unknown\n";
+	}
 }
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index 4f72d27c..55fc4096 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -22,6 +22,8 @@
 #include <liblangutil/Exceptions.h>
 #include <libsolidity/interface/ReadFile.h>
 
+#include <libdevcore/FixedHash.h>
+
 #include <libdevcore/Common.h>
 
 #include <boost/noncopyable.hpp>
@@ -42,7 +44,7 @@ namespace smt
 class SMTLib2Interface: public SolverInterface, public boost::noncopyable
 {
 public:
-	explicit SMTLib2Interface(ReadCallback::Callback const& _queryCallback);
+	explicit SMTLib2Interface(std::map<h256, std::string> const& _queryResponses);
 
 	void reset() override;
 
@@ -54,6 +56,8 @@ public:
 	void addAssertion(Expression const& _expr) override;
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
 
+	std::vector<std::string> unhandledQueries() override { return m_unhandledQueries; }
+
 private:
 	void declareFunction(std::string const&, Sort const&);
 
@@ -69,9 +73,11 @@ private:
 	/// Communicates with the solver via the callback. Throws SMTSolverError on error.
 	std::string querySolver(std::string const& _input);
 
-	ReadCallback::Callback m_queryCallback;
 	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 224e5cd6..2a109b89 100644
--- a/libsolidity/formal/SMTPortfolio.cpp
+++ b/libsolidity/formal/SMTPortfolio.cpp
@@ -23,27 +23,22 @@
 #ifdef HAVE_CVC4
 #include <libsolidity/formal/CVC4Interface.h>
 #endif
-#if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
 #include <libsolidity/formal/SMTLib2Interface.h>
-#endif
 
 using namespace std;
 using namespace dev;
 using namespace dev::solidity;
 using namespace dev::solidity::smt;
 
-SMTPortfolio::SMTPortfolio(ReadCallback::Callback const& _readCallback)
+SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
 {
+	m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses));
 #ifdef HAVE_Z3
 	m_solvers.emplace_back(make_shared<smt::Z3Interface>());
 #endif
 #ifdef HAVE_CVC4
 	m_solvers.emplace_back(make_shared<smt::CVC4Interface>());
 #endif
-#if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
-	m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_readCallback)),
-#endif
-	(void)_readCallback;
 }
 
 void SMTPortfolio::reset()
diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h
index 12e2be66..7f5ba37e 100644
--- a/libsolidity/formal/SMTPortfolio.h
+++ b/libsolidity/formal/SMTPortfolio.h
@@ -22,8 +22,11 @@
 
 #include <libsolidity/interface/ReadFile.h>
 
+#include <libdevcore/FixedHash.h>
+
 #include <boost/noncopyable.hpp>
 
+#include <map>
 #include <vector>
 
 namespace dev
@@ -42,7 +45,7 @@ namespace smt
 class SMTPortfolio: public SolverInterface, public boost::noncopyable
 {
 public:
-	SMTPortfolio(ReadCallback::Callback const& _readCallback);
+	SMTPortfolio(std::map<h256, std::string> const& _smtlib2Responses);
 
 	void reset() override;
 
@@ -54,6 +57,7 @@ public:
 	void addAssertion(Expression const& _expr) override;
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
 
+	std::vector<std::string> unhandledQueries() override { return m_solvers.at(0)->unhandledQueries(); }
 private:
 	static bool solverAnswered(CheckResult result);
 
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index fd1abd61..cc8214de 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -284,6 +284,9 @@ public:
 	virtual std::pair<CheckResult, std::vector<std::string>>
 	check(std::vector<Expression> const& _expressionsToEvaluate) = 0;
 
+	/// @returns a list of queries that the system was not able to respond to.
+	virtual std::vector<std::string> unhandledQueries() { return {}; }
+
 protected:
 	// SMT query timeout in milliseconds.
 	static int const queryTimeout = 10000;
diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp
index a5674705..ae85276e 100644
--- a/libsolidity/interface/CompilerStack.cpp
+++ b/libsolidity/interface/CompilerStack.cpp
@@ -107,6 +107,8 @@ void CompilerStack::reset(bool _keepSources)
 		m_stackState = Empty;
 		m_sources.clear();
 	}
+	m_smtlib2Responses.clear();
+	m_unhandledSMTLib2Queries.clear();
 	m_libraries.clear();
 	m_evmVersion = EVMVersion();
 	m_optimize = false;
@@ -283,9 +285,10 @@ bool CompilerStack::analyze()
 
 		if (noErrors)
 		{
-			SMTChecker smtChecker(m_errorReporter, m_smtQuery);
+			SMTChecker smtChecker(m_errorReporter, m_smtlib2Responses);
 			for (Source const* source: m_sourceOrder)
 				smtChecker.analyze(*source->ast, source->scanner);
+			m_unhandledSMTLib2Queries += smtChecker.unhandledQueries();
 		}
 	}
 	catch(FatalError const&)
diff --git a/libsolidity/interface/CompilerStack.h b/libsolidity/interface/CompilerStack.h
index 8c50266e..2c7add3b 100644
--- a/libsolidity/interface/CompilerStack.h
+++ b/libsolidity/interface/CompilerStack.h
@@ -153,6 +153,9 @@ public:
 	/// @returns true if a source object by the name already existed and was replaced.
 	bool addSource(std::string const& _name, std::string const& _content, bool _isLibrary = false);
 
+	/// 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; }
+
 	/// Parses all source units that were added
 	/// @returns false on error.
 	bool parse();
@@ -188,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;
 
@@ -334,7 +341,6 @@ private:
 	) const;
 
 	ReadCallback::Callback m_readFile;
-	ReadCallback::Callback m_smtQuery;
 	bool m_optimize = false;
 	unsigned m_optimizeRuns = 200;
 	EVMVersion m_evmVersion;
@@ -344,6 +350,8 @@ private:
 	/// "context:prefix=target"
 	std::vector<Remapping> m_remappings;
 	std::map<std::string const, Source> m_sources;
+	std::vector<std::string> m_unhandledSMTLib2Queries;
+	std::map<h256, std::string> m_smtlib2Responses;
 	std::shared_ptr<GlobalContext> m_globalContext;
 	std::vector<Source const*> m_sourceOrder;
 	/// This is updated during compilation.
diff --git a/libsolidity/interface/StandardCompiler.cpp b/libsolidity/interface/StandardCompiler.cpp
index 291a1071..bf33b789 100644
--- a/libsolidity/interface/StandardCompiler.cpp
+++ b/libsolidity/interface/StandardCompiler.cpp
@@ -319,6 +319,27 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
 			return formatFatalError("JSONError", "Invalid input source specified.");
 	}
 
+	Json::Value const& auxInputs = _input["auxiliaryInput"];
+	if (!!auxInputs)
+	{
+		Json::Value const& smtlib2Responses = auxInputs["smtlib2responses"];
+		if (!!smtlib2Responses)
+			for (auto const& hashString: smtlib2Responses.getMemberNames())
+			{
+				h256 hash;
+				try
+				{
+					hash = h256(hashString);
+				}
+				catch (dev::BadHexCharacter const&)
+				{
+					return formatFatalError("JSONError", "Invalid hex encoding of SMTLib2 auxiliary input.");
+				}
+
+				m_compilerStack.addSMTLib2Response(hash, smtlib2Responses[hashString].asString());
+			}
+	}
+
 	Json::Value const& settings = _input.get("settings", Json::Value());
 
 	if (settings.isMember("evmVersion"))
@@ -518,6 +539,10 @@ Json::Value StandardCompiler::compileInternal(Json::Value const& _input)
 	if (errors.size() > 0)
 		output["errors"] = errors;
 
+	if (!m_compilerStack.unhandledSMTLib2Queries().empty())
+		for (string const& query: m_compilerStack.unhandledSMTLib2Queries())
+			output["auxiliaryInputRequested"]["smtlib2queries"]["0x" + keccak256(query).hex()] = query;
+
 	output["sources"] = Json::objectValue;
 	unsigned sourceIndex = 0;
 	for (string const& sourceName: analysisSuccess ? m_compilerStack.sourceNames() : vector<string>())
diff --git a/test/boostTest.cpp b/test/boostTest.cpp
index 5352ef85..6ff6d2d2 100644
--- a/test/boostTest.cpp
+++ b/test/boostTest.cpp
@@ -38,6 +38,7 @@
 #include <test/Options.h>
 #include <test/libsolidity/ASTJSONTest.h>
 #include <test/libsolidity/SyntaxTest.h>
+#include <test/libsolidity/SMTCheckerJSONTest.h>
 #include <test/libyul/YulOptimizerTest.h>
 
 #include <boost/algorithm/string.hpp>
@@ -146,12 +147,21 @@ test_suite* init_unit_test_suite( int /*argc*/, char* /*argv*/[] )
 		dev::yul::test::YulOptimizerTest::create
 	) > 0, "no Yul Optimizer tests found");
 	if (!dev::test::Options::get().disableSMT)
+	{
 		solAssert(registerTests(
 			master,
 			dev::test::Options::get().testPath / "libsolidity",
 			"smtCheckerTests",
 			SyntaxTest::create
 		) > 0, "no SMT checker tests found");
+
+		solAssert(registerTests(
+			master,
+			dev::test::Options::get().testPath / "libsolidity",
+			"smtCheckerTestsJSON",
+			SMTCheckerTest::create
+		) > 0, "no SMT checker JSON tests found");
+	}
 	if (dev::test::Options::get().disableIPC)
 	{
 		for (auto suite: {
diff --git a/test/libsolidity/SMTCheckerJSONTest.cpp b/test/libsolidity/SMTCheckerJSONTest.cpp
new file mode 100644
index 00000000..6e1329a9
--- /dev/null
+++ b/test/libsolidity/SMTCheckerJSONTest.cpp
@@ -0,0 +1,128 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <test/libsolidity/SMTCheckerJSONTest.h>
+#include <test/Options.h>
+#include <libsolidity/interface/StandardCompiler.h>
+#include <libdevcore/JSON.h>
+#include <boost/algorithm/string.hpp>
+#include <boost/algorithm/string/join.hpp>
+#include <boost/algorithm/string/predicate.hpp>
+#include <boost/throw_exception.hpp>
+#include <fstream>
+#include <memory>
+#include <stdexcept>
+#include <sstream>
+
+using namespace dev;
+using namespace solidity;
+using namespace dev::solidity::test;
+using namespace dev::solidity::test::formatting;
+using namespace std;
+using namespace boost::unit_test;
+
+SMTCheckerTest::SMTCheckerTest(string const& _filename)
+: SyntaxTest(_filename)
+{
+	BOOST_REQUIRE_MESSAGE(boost::algorithm::ends_with(_filename, ".sol"), "Invalid test contract file name: \"" + _filename + "\".");
+
+	string jsonFilename = _filename.substr(0, _filename.size() - 4) + ".json";
+	BOOST_CHECK(jsonParseFile(jsonFilename, m_smtResponses));
+	BOOST_CHECK(m_smtResponses.isObject());
+}
+
+bool SMTCheckerTest::run(ostream& _stream, string const& _linePrefix, bool const _formatted)
+{
+	StandardCompiler compiler;
+
+	// Run the compiler and retrieve the smtlib2queries (1st run)
+	string versionPragma = "pragma solidity >=0.0;\n";
+	Json::Value input = buildJson(versionPragma);
+	Json::Value result = compiler.compile(input);
+
+	// This is the list of query hashes requested by the 1st run
+	vector<string> outHashes = hashesFromJson(result, "auxiliaryInputRequested", "smtlib2queries");
+
+	// This is the list of responses provided in the test
+	string auxInput("auxiliaryInput");
+	BOOST_CHECK(m_smtResponses.isMember(auxInput));
+	vector<string> inHashes = hashesFromJson(m_smtResponses, auxInput, "smtlib2responses");
+
+	// Ensure that the provided list matches the requested one
+	BOOST_CHECK_MESSAGE(
+		outHashes == inHashes,
+		"SMT query hashes differ: " + boost::algorithm::join(outHashes, ", ") + " x " + boost::algorithm::join(inHashes, ", ")
+	);
+
+	// Rerun the compiler with the provided hashed (2nd run)
+	input[auxInput] = m_smtResponses[auxInput];
+	Json::Value endResult = compiler.compile(input);
+
+	BOOST_CHECK(endResult.isMember("errors"));
+	Json::Value const& errors = endResult["errors"];
+	for (auto const& error: errors)
+	{
+		BOOST_CHECK(error.isMember("type") && error["type"].isString());
+		BOOST_CHECK(error.isMember("message") && error["message"].isString());
+		if (!error.isMember("sourceLocation"))
+			continue;
+		Json::Value const& location = error["sourceLocation"];
+		BOOST_CHECK(location.isMember("start") && location["start"].isInt());
+		BOOST_CHECK(location.isMember("end") && location["end"].isInt());
+		int start = location["start"].asInt();
+		int end = location["end"].asInt();
+		if (start >= static_cast<int>(versionPragma.size()))
+			start -= versionPragma.size();
+		if (end >= static_cast<int>(versionPragma.size()))
+			end -= versionPragma.size();
+		m_errorList.emplace_back(SyntaxTestError{
+			error["type"].asString(),
+			error["message"].asString(),
+			start,
+			end
+		});
+	}
+
+	return printExpectationAndError(_stream, _linePrefix, _formatted);
+}
+
+vector<string> SMTCheckerTest::hashesFromJson(Json::Value const& _jsonObj, string const& _auxInput, string const& _smtlib)
+{
+	vector<string> hashes;
+	Json::Value const& auxInputs = _jsonObj[_auxInput];
+	if (!!auxInputs)
+	{
+		Json::Value const& smtlib = auxInputs[_smtlib];
+		if (!!smtlib)
+			for (auto const& hashString: smtlib.getMemberNames())
+				hashes.push_back(hashString);
+	}
+	return hashes;
+}
+
+Json::Value SMTCheckerTest::buildJson(string const& _extra)
+{
+	string language = "\"language\": \"Solidity\"";
+	string sourceName = "\"A\"";
+	string sourceContent = "\"" + _extra + m_source + "\"";
+	string sourceObj = "{ \"content\": " + sourceContent + "}";
+	string sources = " \"sources\": { " + sourceName + ": " + sourceObj + "}";
+	string input = "{" + language + ", " + sources + "}";
+	Json::Value source;
+	BOOST_REQUIRE(jsonParse(input, source));
+	return source;
+}
diff --git a/test/libsolidity/SMTCheckerJSONTest.h b/test/libsolidity/SMTCheckerJSONTest.h
new file mode 100644
index 00000000..cf41acac
--- /dev/null
+++ b/test/libsolidity/SMTCheckerJSONTest.h
@@ -0,0 +1,53 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <test/libsolidity/SyntaxTest.h>
+
+#include <libdevcore/JSON.h>
+
+#include <string>
+
+namespace dev
+{
+namespace solidity
+{
+namespace test
+{
+
+class SMTCheckerTest: public SyntaxTest
+{
+public:
+	static std::unique_ptr<TestCase> create(std::string const& _filename)
+	{
+		return std::unique_ptr<TestCase>(new SMTCheckerTest(_filename));
+	}
+	SMTCheckerTest(std::string const& _filename);
+
+	bool run(std::ostream& _stream, std::string const& _linePrefix = "", bool const _formatted = false) override;
+
+private:
+	std::vector<std::string> hashesFromJson(Json::Value const& _jsonObj, std::string const& _auxInput, std::string const& _smtlib);
+	Json::Value buildJson(std::string const& _extra);
+
+	Json::Value m_smtResponses;
+};
+
+}
+}
+}
diff --git a/test/libsolidity/SyntaxTest.cpp b/test/libsolidity/SyntaxTest.cpp
index 45d32b55..c47ea599 100644
--- a/test/libsolidity/SyntaxTest.cpp
+++ b/test/libsolidity/SyntaxTest.cpp
@@ -92,6 +92,11 @@ bool SyntaxTest::run(ostream& _stream, string const& _linePrefix, bool const _fo
 		});
 	}
 
+	return printExpectationAndError(_stream, _linePrefix, _formatted);
+}
+
+bool SyntaxTest::printExpectationAndError(ostream& _stream, string const& _linePrefix, bool const _formatted)
+{
 	if (m_expectations != m_errorList)
 	{
 		string nextIndentLevel = _linePrefix + "  ";
diff --git a/test/libsolidity/SyntaxTest.h b/test/libsolidity/SyntaxTest.h
index 0f151e66..d286f934 100644
--- a/test/libsolidity/SyntaxTest.h
+++ b/test/libsolidity/SyntaxTest.h
@@ -67,7 +67,7 @@ public:
 	}
 
 	static std::string errorMessage(Exception const& _e);
-private:
+protected:
 	static void printErrorList(
 		std::ostream& _stream,
 		std::vector<SyntaxTestError> const& _errors,
@@ -75,6 +75,8 @@ private:
 		bool const _formatted = false
 	);
 
+	virtual bool printExpectationAndError(std::ostream& _stream, std::string const& _linePrefix = "", bool const _formatted = false);
+
 	static std::vector<SyntaxTestError> parseExpectations(std::istream& _stream);
 
 	std::string m_source;
diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json
new file mode 100644
index 00000000..2ed5150d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTestsJSON/multi.json
@@ -0,0 +1,11 @@
+{
+  "auxiliaryInput":
+  {
+	  "smtlib2responses":
+	  {
+		  "0x0426cd198d1e7123a28ffac2b759a666b86508ad046babf5166500dd6d8ed308": "unsat\n(error \"line 31 column 26: model is not available\")",
+		  "0xa51ca41ae407f5a727f27101cbc079834743cc8955f9f585582034ca634953f6": "sat\n((|EVALEXPR_0| 1))",
+		  "0xe9477f683ff20aa57fcb08682150f86c5917e1d4c0686b278ab9b73446d0682c": "sat\n((|EVALEXPR_0| 0))"
+	  }
+  }
+}
diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.sol b/test/libsolidity/smtCheckerTestsJSON/multi.sol
new file mode 100644
index 00000000..e0d69b1d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTestsJSON/multi.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		assert(x > 0);
+		assert(x > 100);
+		assert(x >= 0);
+	}
+}
+// ----
+// Warning: (82-95): Assertion violation happens here
+// Warning: (99-114): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.json b/test/libsolidity/smtCheckerTestsJSON/simple.json
new file mode 100644
index 00000000..fd976b63
--- /dev/null
+++ b/test/libsolidity/smtCheckerTestsJSON/simple.json
@@ -0,0 +1,9 @@
+{
+  "auxiliaryInput":
+  {
+	  "smtlib2responses":
+	  {
+		  "0xe9477f683ff20aa57fcb08682150f86c5917e1d4c0686b278ab9b73446d0682c": "sat\n((|EVALEXPR_0| 0))"
+	  }
+  }
+}
diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.sol b/test/libsolidity/smtCheckerTestsJSON/simple.sol
new file mode 100644
index 00000000..6bc7193d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTestsJSON/simple.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x) public pure {
+		assert(x > 0);
+	}
+}
+// ----
+// Warning: (82-95): Assertion violation happens here
diff --git a/test/tools/CMakeLists.txt b/test/tools/CMakeLists.txt
index 19a1d958..a0fbe140 100644
--- a/test/tools/CMakeLists.txt
+++ b/test/tools/CMakeLists.txt
@@ -6,5 +6,5 @@ target_link_libraries(yulopti PRIVATE solidity ${Boost_PROGRAM_OPTIONS_LIBRARIES
 
 add_executable(isoltest isoltest.cpp ../Options.cpp ../Common.cpp ../libsolidity/TestCase.cpp ../libsolidity/SyntaxTest.cpp
         ../libsolidity/AnalysisFramework.cpp ../libsolidity/SolidityExecutionFramework.cpp ../ExecutionFramework.cpp
-        ../RPCSession.cpp ../libsolidity/ASTJSONTest.cpp ../libyul/YulOptimizerTest.cpp)
+        ../RPCSession.cpp ../libsolidity/ASTJSONTest.cpp ../libsolidity/SMTCheckerJSONTest.cpp ../libyul/YulOptimizerTest.cpp)
 target_link_libraries(isoltest PRIVATE libsolc solidity evmasm ${Boost_PROGRAM_OPTIONS_LIBRARIES} ${Boost_UNIT_TEST_FRAMEWORK_LIBRARIES})
diff --git a/test/tools/isoltest.cpp b/test/tools/isoltest.cpp
index 1b6fd54a..f8e2dc58 100644
--- a/test/tools/isoltest.cpp
+++ b/test/tools/isoltest.cpp
@@ -21,6 +21,7 @@
 #include <test/libsolidity/AnalysisFramework.h>
 #include <test/libsolidity/SyntaxTest.h>
 #include <test/libsolidity/ASTJSONTest.h>
+#include <test/libsolidity/SMTCheckerJSONTest.h>
 #include <test/libyul/YulOptimizerTest.h>
 
 #include <boost/algorithm/string.hpp>
@@ -412,6 +413,17 @@ Allowed options)",
 			global_stats += *stats;
 		else
 			return 1;
+
+		if (auto stats = runTestSuite(
+			"SMT Checker JSON",
+			testPath / "libsolidity",
+			"smtCheckerTestsJSON",
+			SMTCheckerTest::create,
+			formatted
+		))
+			global_stats += *stats;
+		else
+			return 1;
 	}
 
 	cout << endl << "Summary: ";