diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt
index 81e86e621..714c3c766 100644
--- a/libsolidity/CMakeLists.txt
+++ b/libsolidity/CMakeLists.txt
@@ -79,6 +79,8 @@ set(sources
 	formal/BMC.h
 	formal/CHC.cpp
 	formal/CHC.h
+	formal/CHCSmtLib2Interface.cpp
+	formal/CHCSmtLib2Interface.h
 	formal/CHCSolverInterface.h
 	formal/EncodingContext.cpp
 	formal/EncodingContext.h
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 8d81198dd..22d70a5aa 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -17,6 +17,8 @@
 
 #include <libsolidity/formal/CHC.h>
 
+#include <libsolidity/formal/CHCSmtLib2Interface.h>
+
 #ifdef HAVE_Z3
 #include <libsolidity/formal/Z3CHCInterface.h>
 #endif
@@ -30,13 +32,20 @@ using namespace dev;
 using namespace langutil;
 using namespace dev::solidity;
 
-CHC::CHC(smt::EncodingContext& _context, ErrorReporter& _errorReporter):
+CHC::CHC(
+	smt::EncodingContext& _context,
+	ErrorReporter& _errorReporter,
+	map<h256, string> const& _smtlib2Responses
+):
 	SMTEncoder(_context),
 #ifdef HAVE_Z3
 	m_interface(make_shared<smt::Z3CHCInterface>()),
+#else
+	m_interface(make_shared<smt::CHCSmtLib2Interface>(_smtlib2Responses)),
 #endif
 	m_outerErrorReporter(_errorReporter)
 {
+	(void)_smtlib2Responses;
 }
 
 void CHC::analyze(SourceUnit const& _source)
@@ -47,12 +56,24 @@ void CHC::analyze(SourceUnit const& _source)
 	auto z3Interface = dynamic_pointer_cast<smt::Z3CHCInterface>(m_interface);
 	solAssert(z3Interface, "");
 	m_context.setSolver(z3Interface->z3Interface());
+#else
+	auto smtlib2Interface = dynamic_pointer_cast<smt::CHCSmtLib2Interface>(m_interface);
+	solAssert(smtlib2Interface, "");
+	m_context.setSolver(smtlib2Interface->smtlib2Interface());
+#endif
 	m_context.clear();
 	m_context.setAssertionAccumulation(false);
 	m_variableUsage.setFunctionInlining(false);
 
 	_source.accept(*this);
-#endif
+}
+
+vector<string> CHC::unhandledQueries() const
+{
+	if (auto smtlib2 = dynamic_pointer_cast<smt::CHCSmtLib2Interface>(m_interface))
+		return smtlib2->unhandledQueries();
+
+	return {};
 }
 
 bool CHC::visit(ContractDefinition const& _contract)
@@ -99,7 +120,7 @@ bool CHC::visit(ContractDefinition const& _contract)
 		{
 			auto const& symbVar = m_context.variable(*var);
 			symbVar->increaseIndex();
-			m_interface->declareVariable(symbVar->currentName(), *symbVar->sort());
+			m_interface->declareVariable(symbVar->currentName(), symbVar->sort());
 			m_context.setZeroValue(*symbVar);
 		}
 
diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h
index 308f1a610..965da2d79 100644
--- a/libsolidity/formal/CHC.h
+++ b/libsolidity/formal/CHC.h
@@ -44,12 +44,21 @@ namespace solidity
 class CHC: public SMTEncoder
 {
 public:
-	CHC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter);
+	CHC(
+		smt::EncodingContext& _context,
+		langutil::ErrorReporter& _errorReporter,
+		std::map<h256, std::string> const& _smtlib2Responses
+	);
 
 	void analyze(SourceUnit const& _sources);
 
 	std::set<Expression const*> const& safeAssertions() const { return m_safeAssertions; }
 
+	/// This is used if the Horn solver is not directly linked into this binary.
+	/// @returns a list of inputs to the Horn solver that were not part of the argument to
+	/// the constructor.
+	std::vector<std::string> unhandledQueries() const;
+
 private:
 	/// Visitor functions.
 	//@{
diff --git a/libsolidity/formal/CHCSmtLib2Interface.cpp b/libsolidity/formal/CHCSmtLib2Interface.cpp
new file mode 100644
index 000000000..fb424d782
--- /dev/null
+++ b/libsolidity/formal/CHCSmtLib2Interface.cpp
@@ -0,0 +1,160 @@
+/*
+	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 <libsolidity/formal/CHCSmtLib2Interface.h>
+
+#include <libdevcore/Keccak256.h>
+
+#include <boost/algorithm/string/join.hpp>
+#include <boost/algorithm/string/predicate.hpp>
+#include <boost/filesystem/operations.hpp>
+
+#include <array>
+#include <fstream>
+#include <iostream>
+#include <memory>
+#include <stdexcept>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+using namespace dev::solidity::smt;
+
+CHCSmtLib2Interface::CHCSmtLib2Interface(map<h256, string> const& _queryResponses):
+	m_smtlib2(make_shared<SMTLib2Interface>(_queryResponses)),
+	m_queryResponses(_queryResponses)
+{
+	reset();
+}
+
+void CHCSmtLib2Interface::reset()
+{
+	m_accumulatedOutput.clear();
+	m_variables.clear();
+}
+
+void CHCSmtLib2Interface::registerRelation(smt::Expression const& _expr)
+{
+	solAssert(_expr.sort, "");
+	solAssert(_expr.sort->kind == smt::Kind::Function, "");
+	if (!m_variables.count(_expr.name))
+	{
+		auto fSort = dynamic_pointer_cast<FunctionSort>(_expr.sort);
+		string domain = m_smtlib2->toSmtLibSort(fSort->domain);
+		// Relations are predicates which have implicit codomain Bool.
+		m_variables.insert(_expr.name);
+		write(
+			"(declare-rel |" +
+			_expr.name +
+			"| " +
+			domain +
+			")"
+		);
+	}
+}
+
+void CHCSmtLib2Interface::addRule(smt::Expression const& _expr, std::string const& _name)
+{
+	write(
+		"(rule (! " +
+		m_smtlib2->toSExpr(_expr) +
+		" :named " +
+		_name +
+		"))"
+	);
+}
+
+pair<CheckResult, vector<string>> CHCSmtLib2Interface::query(smt::Expression const& _block)
+{
+	string accumulated{};
+	swap(m_accumulatedOutput, accumulated);
+	for (auto const& var: m_smtlib2->variables())
+		declareVariable(var.first, var.second);
+	m_accumulatedOutput += accumulated;
+
+	string response = querySolver(
+		m_accumulatedOutput +
+		"\n(query " + _block.name + " :print-certificate true)"
+	);
+
+	CheckResult result;
+	// TODO proper parsing
+	if (boost::starts_with(response, "sat\n"))
+		result = CheckResult::SATISFIABLE;
+	else if (boost::starts_with(response, "unsat\n"))
+		result = CheckResult::UNSATISFIABLE;
+	else if (boost::starts_with(response, "unknown\n"))
+		result = CheckResult::UNKNOWN;
+	else
+		result = CheckResult::ERROR;
+
+	// TODO collect invariants or counterexamples.
+	return make_pair(result, vector<string>{});
+}
+
+void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)
+{
+	solAssert(_sort, "");
+	if (_sort->kind == Kind::Function)
+		declareFunction(_name, _sort);
+	else if (!m_variables.count(_name))
+	{
+		m_variables.insert(_name);
+		write("(declare-var |" + _name + "| " + m_smtlib2->toSmtLibSort(*_sort) + ')');
+	}
+}
+
+void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)
+{
+	solAssert(_sort, "");
+	solAssert(_sort->kind == smt::Kind::Function, "");
+	// TODO Use domain and codomain as key as well
+	if (!m_variables.count(_name))
+	{
+		auto fSort = dynamic_pointer_cast<FunctionSort>(_sort);
+		solAssert(fSort->codomain, "");
+		string domain = m_smtlib2->toSmtLibSort(fSort->domain);
+		string codomain = m_smtlib2->toSmtLibSort(*fSort->codomain);
+		m_variables.insert(_name);
+		write(
+			"(declare-fun |" +
+			_name +
+			"| " +
+			domain +
+			" " +
+			codomain +
+			")"
+		);
+	}
+}
+
+void CHCSmtLib2Interface::write(string _data)
+{
+	m_accumulatedOutput += move(_data) + "\n";
+}
+
+string CHCSmtLib2Interface::querySolver(string const& _input)
+{
+	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/CHCSmtLib2Interface.h b/libsolidity/formal/CHCSmtLib2Interface.h
new file mode 100644
index 000000000..22bbba859
--- /dev/null
+++ b/libsolidity/formal/CHCSmtLib2Interface.h
@@ -0,0 +1,75 @@
+/*
+	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/>.
+*/
+
+/**
+ * Interface for solving Horn systems via smtlib2.
+ */
+
+#pragma once
+
+#include <libsolidity/formal/CHCSolverInterface.h>
+
+#include <libsolidity/formal/SMTLib2Interface.h>
+
+namespace dev
+{
+namespace solidity
+{
+namespace smt
+{
+
+class CHCSmtLib2Interface: public CHCSolverInterface
+{
+public:
+	explicit CHCSmtLib2Interface(std::map<h256, std::string> const& _queryResponses);
+
+	void reset();
+
+	void registerRelation(Expression const& _expr) override;
+
+	void addRule(Expression const& _expr, std::string const& _name) override;
+
+	std::pair<CheckResult, std::vector<std::string>> query(Expression const& _expr) override;
+
+	void declareVariable(std::string const& _name, SortPointer const& _sort) override;
+
+	std::vector<std::string> unhandledQueries() const { return m_unhandledQueries; }
+
+	std::shared_ptr<SMTLib2Interface> smtlib2Interface() { return m_smtlib2; }
+
+private:
+	void declareFunction(std::string const& _name, SortPointer const& _sort);
+
+	void write(std::string _data);
+
+	/// Communicates with the solver via the callback. Throws SMTSolverError on error.
+	std::string querySolver(std::string const& _input);
+
+	/// Used to access toSmtLibSort, SExpr, and handle variables.
+	/// Needs to be a shared_ptr since it's also passed to EncodingContext.
+	std::shared_ptr<SMTLib2Interface> m_smtlib2;
+
+	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/CHCSolverInterface.h b/libsolidity/formal/CHCSolverInterface.h
index 091aa3d7c..0862adaff 100644
--- a/libsolidity/formal/CHCSolverInterface.h
+++ b/libsolidity/formal/CHCSolverInterface.h
@@ -35,7 +35,7 @@ class CHCSolverInterface
 public:
 	virtual ~CHCSolverInterface() = default;
 
-	virtual void declareVariable(std::string const& _name, Sort const& _sort) = 0;
+	virtual void declareVariable(std::string const& _name, SortPointer const& _sort) = 0;
 
 	/// Takes a function declaration as a relation.
 	virtual void registerRelation(Expression const& _expr) = 0;
diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp
index f51f23b97..377df32d2 100644
--- a/libsolidity/formal/CVC4Interface.cpp
+++ b/libsolidity/formal/CVC4Interface.cpp
@@ -48,9 +48,10 @@ void CVC4Interface::pop()
 	m_solver.pop();
 }
 
-void CVC4Interface::declareVariable(string const& _name, Sort const& _sort)
+void CVC4Interface::declareVariable(string const& _name, SortPointer const& _sort)
 {
-	m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(_sort));
+	solAssert(_sort, "");
+	m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(*_sort));
 }
 
 void CVC4Interface::addAssertion(Expression const& _expr)
diff --git a/libsolidity/formal/CVC4Interface.h b/libsolidity/formal/CVC4Interface.h
index 897923647..28596bdcf 100644
--- a/libsolidity/formal/CVC4Interface.h
+++ b/libsolidity/formal/CVC4Interface.h
@@ -50,7 +50,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareVariable(std::string const&, Sort const&) override;
+	void declareVariable(std::string const&, SortPointer const&) override;
 
 	void addAssertion(Expression const& _expr) override;
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp
index 265d0f991..c061c8416 100644
--- a/libsolidity/formal/ModelChecker.cpp
+++ b/libsolidity/formal/ModelChecker.cpp
@@ -24,7 +24,7 @@ using namespace dev::solidity;
 
 ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
 	m_bmc(m_context, _errorReporter, _smtlib2Responses),
-	m_chc(m_context, _errorReporter),
+	m_chc(m_context, _errorReporter, _smtlib2Responses),
 	m_context()
 {
 }
@@ -40,5 +40,5 @@ void ModelChecker::analyze(SourceUnit const& _source)
 
 vector<string> ModelChecker::unhandledQueries()
 {
-	return m_bmc.unhandledQueries();
+	return m_bmc.unhandledQueries() + m_chc.unhandledQueries();
 }
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index c0d37431e..3c0f38601 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -60,27 +60,29 @@ void SMTLib2Interface::pop()
 	m_accumulatedOutput.pop_back();
 }
 
-void SMTLib2Interface::declareVariable(string const& _name, Sort const& _sort)
+void SMTLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)
 {
-	if (_sort.kind == Kind::Function)
+	solAssert(_sort, "");
+	if (_sort->kind == Kind::Function)
 		declareFunction(_name, _sort);
 	else if (!m_variables.count(_name))
 	{
-		m_variables.insert(_name);
-		write("(declare-fun |" + _name + "| () " + toSmtLibSort(_sort) + ')');
+		m_variables.emplace(_name, _sort);
+		write("(declare-fun |" + _name + "| () " + toSmtLibSort(*_sort) + ')');
 	}
 }
 
-void SMTLib2Interface::declareFunction(string const& _name, Sort const& _sort)
+void SMTLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)
 {
-	solAssert(_sort.kind == smt::Kind::Function, "");
+	solAssert(_sort, "");
+	solAssert(_sort->kind == smt::Kind::Function, "");
 	// TODO Use domain and codomain as key as well
 	if (!m_variables.count(_name))
 	{
-		FunctionSort fSort = dynamic_cast<FunctionSort const&>(_sort);
-		string domain = toSmtLibSort(fSort.domain);
-		string codomain = toSmtLibSort(*fSort.codomain);
-		m_variables.insert(_name);
+		auto const& fSort = dynamic_pointer_cast<FunctionSort>(_sort);
+		string domain = toSmtLibSort(fSort->domain);
+		string codomain = toSmtLibSort(*fSort->codomain);
+		m_variables.emplace(_name, _sort);
 		write(
 			"(declare-fun |" +
 			_name +
@@ -159,6 +161,7 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 	case Kind::Array:
 	{
 		auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
+		solAssert(arraySort.domain && arraySort.range, "");
 		return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')';
 	}
 	default:
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index a39c861c6..21c11f80d 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -48,20 +48,23 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareVariable(std::string const&, Sort const&) override;
+	void declareVariable(std::string const&, SortPointer const&) override;
 
 	void addAssertion(smt::Expression const& _expr) override;
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<smt::Expression> const& _expressionsToEvaluate) override;
 
 	std::vector<std::string> unhandledQueries() override { return m_unhandledQueries; }
 
-private:
-	void declareFunction(std::string const&, Sort const&);
-
+	// Used by CHCSmtLib2Interface
 	std::string toSExpr(smt::Expression const& _expr);
 	std::string toSmtLibSort(Sort const& _sort);
 	std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
 
+	std::map<std::string, SortPointer> variables() { return m_variables; }
+
+private:
+	void declareFunction(std::string const& _name, SortPointer const& _sort);
+
 	void write(std::string _data);
 
 	std::string checkSatAndGetValuesCommand(std::vector<smt::Expression> const& _expressionsToEvaluate);
@@ -71,7 +74,7 @@ private:
 	std::string querySolver(std::string const& _input);
 
 	std::vector<std::string> m_accumulatedOutput;
-	std::set<std::string> m_variables;
+	std::map<std::string, SortPointer> 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 73c194a01..d47c01f31 100644
--- a/libsolidity/formal/SMTPortfolio.cpp
+++ b/libsolidity/formal/SMTPortfolio.cpp
@@ -59,8 +59,9 @@ void SMTPortfolio::pop()
 		s->pop();
 }
 
-void SMTPortfolio::declareVariable(string const& _name, Sort const& _sort)
+void SMTPortfolio::declareVariable(string const& _name, SortPointer const& _sort)
 {
+	solAssert(_sort, "");
 	for (auto const& s: m_solvers)
 		s->declareVariable(_name, _sort);
 }
diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h
index ded7985f9..d922affd2 100644
--- a/libsolidity/formal/SMTPortfolio.h
+++ b/libsolidity/formal/SMTPortfolio.h
@@ -49,7 +49,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareVariable(std::string const&, Sort const&) override;
+	void declareVariable(std::string const&, SortPointer const&) override;
 
 	void addAssertion(smt::Expression const& _expr) override;
 
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 0004e1726..2889af25a 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -338,13 +338,13 @@ public:
 	virtual void push() = 0;
 	virtual void pop() = 0;
 
-	virtual void declareVariable(std::string const& _name, Sort const& _sort) = 0;
-	Expression newVariable(std::string _name, SortPointer _sort)
+	virtual void declareVariable(std::string const& _name, SortPointer const& _sort) = 0;
+	Expression newVariable(std::string _name, SortPointer const& _sort)
 	{
 		// Subclasses should do something here
 		solAssert(_sort, "");
-		declareVariable(_name, *_sort);
-		return Expression(std::move(_name), {}, std::move(_sort));
+		declareVariable(_name, _sort);
+		return Expression(std::move(_name), {}, _sort);
 	}
 
 	virtual void addAssertion(Expression const& _expr) = 0;
diff --git a/libsolidity/formal/Z3CHCInterface.cpp b/libsolidity/formal/Z3CHCInterface.cpp
index 100a1fb7d..87d0db0c4 100644
--- a/libsolidity/formal/Z3CHCInterface.cpp
+++ b/libsolidity/formal/Z3CHCInterface.cpp
@@ -47,8 +47,9 @@ Z3CHCInterface::Z3CHCInterface():
 	m_solver.set(p);
 }
 
-void Z3CHCInterface::declareVariable(string const& _name, Sort const& _sort)
+void Z3CHCInterface::declareVariable(string const& _name, SortPointer const& _sort)
 {
+	solAssert(_sort, "");
 	m_z3Interface->declareVariable(_name, _sort);
 }
 
diff --git a/libsolidity/formal/Z3CHCInterface.h b/libsolidity/formal/Z3CHCInterface.h
index a107ad424..3acab97c3 100644
--- a/libsolidity/formal/Z3CHCInterface.h
+++ b/libsolidity/formal/Z3CHCInterface.h
@@ -37,7 +37,7 @@ public:
 	Z3CHCInterface();
 
 	/// Forwards variable declaration to Z3Interface.
-	void declareVariable(std::string const& _name, Sort const& _sort) override;
+	void declareVariable(std::string const& _name, SortPointer const& _sort) override;
 
 	void registerRelation(Expression const& _expr) override;
 
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index ed3ae0fd9..aa20eb533 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -50,14 +50,15 @@ void Z3Interface::pop()
 	m_solver.pop();
 }
 
-void Z3Interface::declareVariable(string const& _name, Sort const& _sort)
+void Z3Interface::declareVariable(string const& _name, SortPointer const& _sort)
 {
-	if (_sort.kind == Kind::Function)
-		declareFunction(_name, _sort);
+	solAssert(_sort, "");
+	if (_sort->kind == Kind::Function)
+		declareFunction(_name, *_sort);
 	else if (m_constants.count(_name))
-		m_constants.at(_name) = m_context.constant(_name.c_str(), z3Sort(_sort));
+		m_constants.at(_name) = m_context.constant(_name.c_str(), z3Sort(*_sort));
 	else
-		m_constants.emplace(_name, m_context.constant(_name.c_str(), z3Sort(_sort)));
+		m_constants.emplace(_name, m_context.constant(_name.c_str(), z3Sort(*_sort)));
 }
 
 void Z3Interface::declareFunction(string const& _name, Sort const& _sort)
diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h
index 171fdcaa5..38734dd00 100644
--- a/libsolidity/formal/Z3Interface.h
+++ b/libsolidity/formal/Z3Interface.h
@@ -38,7 +38,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareVariable(std::string const& _name, Sort const& _sort) override;
+	void declareVariable(std::string const& _name, SortPointer const& _sort) override;
 
 	void addAssertion(Expression const& _expr) override;
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;