3 files changed, 38 insertions, 2 deletions
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..3fceed24 100644
--- a/libsolidity/interface/CompilerStack.h
+++ b/libsolidity/interface/CompilerStack.h
@@ -153,6 +153,13 @@ 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; }
+
+	/// @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();
@@ -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..59c28cd9 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["smtlib2"];
+		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.unhandledSMTQueries().empty())
+		for (string const& query: m_compilerStack.unhandledSMTQueries())
+			output["auxiliaryInputRequested"]["smtlib2"]["0x" + keccak256(query).hex()] = query;
+
 	output["sources"] = Json::objectValue;
 	unsigned sourceIndex = 0;
 	for (string const& sourceName: analysisSuccess ? m_compilerStack.sourceNames() : vector<string>())