diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp
index 150b5813d..2442c7df7 100644
--- a/libsolidity/formal/EncodingContext.cpp
+++ b/libsolidity/formal/EncodingContext.cpp
@@ -23,15 +23,15 @@ using namespace std;
 using namespace dev;
 using namespace dev::solidity::smt;
 
-EncodingContext::EncodingContext(SolverInterface& _solver):
-	m_solver(_solver),
-	m_thisAddress(make_unique<SymbolicAddressVariable>("this", m_solver))
+EncodingContext::EncodingContext(std::shared_ptr<SolverInterface> _solver):
+	m_thisAddress(make_unique<SymbolicAddressVariable>("this", *_solver)),
+	m_solver(_solver)
 {
 	auto sort = make_shared<ArraySort>(
 		make_shared<Sort>(Kind::Int),
 		make_shared<Sort>(Kind::Int)
 	);
-	m_balances = make_unique<SymbolicVariable>(sort, "balances", m_solver);
+	m_balances = make_unique<SymbolicVariable>(sort, "balances", *m_solver);
 }
 
 void EncodingContext::reset()
@@ -41,6 +41,7 @@ void EncodingContext::reset()
 	m_globalContext.clear();
 	m_thisAddress->increaseIndex();
 	m_balances->increaseIndex();
+	m_assertions.clear();
 }
 
 /// Variables.
@@ -55,7 +56,7 @@ bool EncodingContext::createVariable(solidity::VariableDeclaration const& _varDe
 {
 	solAssert(!knownVariable(_varDecl), "");
 	auto const& type = _varDecl.type();
-	auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), m_solver);
+	auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_solver);
 	m_variables.emplace(&_varDecl, result.second);
 	return result.first;
 }
@@ -105,7 +106,7 @@ void EncodingContext::setZeroValue(solidity::VariableDeclaration const& _decl)
 
 void EncodingContext::setZeroValue(SymbolicVariable& _variable)
 {
-	setSymbolicZeroValue(_variable, m_solver);
+	setSymbolicZeroValue(_variable, *m_solver);
 }
 
 void EncodingContext::setUnknownValue(solidity::VariableDeclaration const& _decl)
@@ -116,7 +117,7 @@ void EncodingContext::setUnknownValue(solidity::VariableDeclaration const& _decl
 
 void EncodingContext::setUnknownValue(SymbolicVariable& _variable)
 {
-	setSymbolicUnknownValue(_variable, m_solver);
+	setSymbolicUnknownValue(_variable, *m_solver);
 }
 
 /// Expressions
@@ -143,7 +144,7 @@ bool EncodingContext::createExpression(solidity::Expression const& _e, shared_pt
 	}
 	else
 	{
-		auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), m_solver);
+		auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_solver);
 		m_expressions.emplace(&_e, result.second);
 		return result.first;
 	}
@@ -165,7 +166,7 @@ shared_ptr<SymbolicVariable> EncodingContext::globalSymbol(string const& _name)
 bool EncodingContext::createGlobalSymbol(string const& _name, solidity::Expression const& _expr)
 {
 	solAssert(!knownGlobalSymbol(_name), "");
-	auto result = newSymbolicVariable(*_expr.annotation().type, _name, m_solver);
+	auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_solver);
 	m_globalContext.emplace(_name, result.second);
 	setUnknownValue(*result.second);
 	return result.first;
@@ -207,9 +208,40 @@ void EncodingContext::transfer(Expression _from, Expression _to, Expression _val
 		m_balances->valueAtIndex(indexBefore),
 		m_balances->valueAtIndex(indexAfter)
 	);
-	m_solver.addAssertion(m_balances->currentValue() == newBalances);
+	m_solver->addAssertion(m_balances->currentValue() == newBalances);
 }
 
+/// Solver.
+
+Expression EncodingContext::assertions()
+{
+	if (m_assertions.empty())
+		return Expression(true);
+
+	return m_assertions.back();
+}
+
+void EncodingContext::pushSolver()
+{
+	m_assertions.push_back(assertions());
+}
+
+void EncodingContext::popSolver()
+{
+	solAssert(!m_assertions.empty(), "");
+	m_assertions.pop_back();
+}
+
+void EncodingContext::addAssertion(Expression const& _expr)
+{
+	if (m_assertions.empty())
+		m_assertions.push_back(_expr);
+	else
+		m_assertions.back() = _expr && move(m_assertions.back());
+}
+
+/// Private helpers.
+
 void EncodingContext::addBalance(Expression _address, Expression _value)
 {
 	auto newBalances = Expression::store(
@@ -218,5 +250,5 @@ void EncodingContext::addBalance(Expression _address, Expression _value)
 		balance(_address) + move(_value)
 	);
 	m_balances->increaseIndex();
-	m_solver.addAssertion(newBalances == m_balances->currentValue());
+	m_solver->addAssertion(newBalances == m_balances->currentValue());
 }
diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h
index 4a7d05863..4532d6fb4 100644
--- a/libsolidity/formal/EncodingContext.h
+++ b/libsolidity/formal/EncodingContext.h
@@ -36,12 +36,12 @@ namespace smt
 class EncodingContext
 {
 public:
-	EncodingContext(SolverInterface& _solver);
+	EncodingContext(std::shared_ptr<SolverInterface> _solver);
 
 	/// Resets the entire context.
 	void reset();
 
-	/// Methods related to variables.
+	/// Variables.
 	//@{
 	/// @returns the symbolic representation of a program variable.
 	std::shared_ptr<SymbolicVariable> variable(solidity::VariableDeclaration const& _varDecl);
@@ -74,7 +74,7 @@ public:
 	void setUnknownValue(SymbolicVariable& _variable);
 	//@}
 
-	/// Methods related to expressions.
+	/// Expressions.
 	////@{
 	/// @returns the symbolic representation of an AST node expression.
 	std::shared_ptr<SymbolicVariable> expression(solidity::Expression const& _e);
@@ -88,12 +88,13 @@ public:
 	bool knownExpression(solidity::Expression const& _e) const;
 	//@}
 
-	/// Methods related to global variables and functions.
+	/// Global variables and functions.
 	//@{
 	/// Global variables and functions.
 	std::shared_ptr<SymbolicVariable> globalSymbol(std::string const& _name);
-	/// @returns all symbolic variables.
+	/// @returns all symbolic globals.
 	std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> const& globalSymbols() const { return m_globalContext; }
+
 	/// Defines a new global variable or function
 	/// and @returns true if type was abstracted.
 	bool createGlobalSymbol(std::string const& _name, solidity::Expression const& _expr);
@@ -101,7 +102,7 @@ public:
 	bool knownGlobalSymbol(std::string const& _var) const;
 	//@}
 
-	/// Blockchain related methods.
+	/// Blockchain.
 	//@{
 	/// Value of `this` address.
 	Expression thisAddress();
@@ -113,12 +114,22 @@ public:
 	void transfer(Expression _from, Expression _to, Expression _value);
 	//@}
 
+	/// Solver.
+	//@{
+	/// @returns conjunction of all added assertions.
+	Expression assertions();
+	void pushSolver();
+	void popSolver();
+	void addAssertion(Expression const& _e);
+	std::shared_ptr<SolverInterface> solver() { return m_solver; }
+	//@}
+
 private:
 	/// Adds _value to _account's balance.
 	void addBalance(Expression _account, Expression _value);
 
-	SolverInterface& m_solver;
-
+	/// Symbolic expressions.
+	//{@
 	/// Symbolic variables.
 	std::unordered_map<solidity::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
 
@@ -134,6 +145,16 @@ private:
 
 	/// Symbolic balances.
 	std::unique_ptr<SymbolicVariable> m_balances;
+	//@}
+
+	/// Solver related.
+	//@{
+	/// Solver can be SMT solver or Horn solver in the future.
+	std::shared_ptr<SolverInterface> m_solver;
+
+	/// Assertion stack.
+	std::vector<Expression> m_assertions;
+	//@}
 };
 
 }
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 38caa566b..484a3afaf 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -34,7 +34,7 @@ using namespace langutil;
 using namespace dev::solidity;
 
 SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
-	m_interface(_smtlib2Responses),
+	m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses)),
 	m_errorReporterReference(_errorReporter),
 	m_errorReporter(m_smtErrors),
 	m_context(m_interface)
@@ -59,11 +59,11 @@ void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _
 
 	_source.accept(*this);
 
-	solAssert(m_interface.solvers() > 0, "");
+	solAssert(m_interface->solvers() > 0, "");
 	// If this check is true, Z3 and CVC4 are not available
 	// and the query answers were not provided, since SMTPortfolio
 	// guarantees that SmtLib2Interface is the first solver.
-	if (!m_interface.unhandledQueries().empty() && m_interface.solvers() == 1)
+	if (!m_interface->unhandledQueries().empty() && m_interface->solvers() == 1)
 	{
 		if (!m_noSolverWarning)
 		{
@@ -109,7 +109,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 	// Not visited by a function call
 	if (m_callStack.empty())
 	{
-		m_interface.reset();
+		m_interface->reset();
 		m_context.reset();
 		m_pathConditions.clear();
 		m_callStack.clear();
@@ -305,13 +305,13 @@ bool SMTChecker::visit(ForStatement const& _node)
 			checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
 	}
 
-	m_interface.push();
+	m_interface->push();
 	if (_node.condition())
-		m_interface.addAssertion(expr(*_node.condition()));
+		m_interface->addAssertion(expr(*_node.condition()));
 	_node.body().accept(*this);
 	if (_node.loopExpression())
 		_node.loopExpression()->accept(*this);
-	m_interface.pop();
+	m_interface->pop();
 
 	auto indicesAfterLoop = copyVariableIndices();
 	// We reset the execution to before the loop
@@ -696,7 +696,7 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 		solAssert(value, "");
 
 		smt::Expression thisBalance = m_context.balance();
-		setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_interface);
+		setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), *m_interface);
 		checkCondition(thisBalance < expr(*value), _funCall.location(), "Insufficient funds", "address(this).balance", &thisBalance);
 
 		m_context.transfer(m_context.thisAddress(), expr(address), expr(*value));
@@ -740,7 +740,7 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 	// We set the current value to unknown anyway to add type constraints.
 	m_context.setUnknownValue(*symbolicVar);
 	if (index > 0)
-		m_interface.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
+		m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
 }
 
 void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
@@ -822,7 +822,7 @@ void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall)
 		smtArguments.push_back(expr(*arg));
 	defineExpr(_funCall, (*m_context.expression(_funCall.expression()))(smtArguments));
 	m_uninterpretedTerms.insert(&_funCall);
-	setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, m_interface);
+	setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, *m_interface);
 }
 
 void SMTChecker::endVisit(Identifier const& _identifier)
@@ -914,7 +914,7 @@ void SMTChecker::endVisit(Literal const& _literal)
 			auto stringType = TypeProvider::stringMemory();
 			auto stringLit = dynamic_cast<StringLiteralType const*>(_literal.annotation().type);
 			solAssert(stringLit, "");
-			auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), m_interface);
+			auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface);
 			m_context.createExpression(_literal, result.second);
 		}
 		m_errorReporter.warning(
@@ -939,10 +939,10 @@ void SMTChecker::endVisit(Return const& _return)
 			solAssert(components.size() == returnParams.size(), "");
 			for (unsigned i = 0; i < returnParams.size(); ++i)
 				if (components.at(i))
-					m_interface.addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i)));
+					m_interface->addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i)));
 		}
 		else if (returnParams.size() == 1)
-			m_interface.addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front()));
+			m_interface->addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front()));
 	}
 }
 
@@ -984,7 +984,7 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
 		if (_memberAccess.memberName() == "balance")
 		{
 			defineExpr(_memberAccess, m_context.balance(expr(_memberAccess.expression())));
-			setSymbolicUnknownValue(*m_context.expression(_memberAccess), m_interface);
+			setSymbolicUnknownValue(*m_context.expression(_memberAccess), *m_interface);
 			m_uninterpretedTerms.insert(&_memberAccess);
 			return false;
 		}
@@ -1031,7 +1031,7 @@ void SMTChecker::endVisit(IndexAccess const& _indexAccess)
 	setSymbolicUnknownValue(
 		expr(_indexAccess),
 		_indexAccess.annotation().type,
-		m_interface
+		*m_interface
 	);
 	m_uninterpretedTerms.insert(&_indexAccess);
 }
@@ -1083,7 +1083,7 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 			expr(*indexAccess.indexExpression()),
 			_rightHandSide
 		);
-		m_interface.addAssertion(m_context.newValue(*varDecl) == store);
+		m_interface->addAssertion(m_context.newValue(*varDecl) == store);
 		// Update the SMT select value after the assignment,
 		// necessary for sound models.
 		defineExpr(indexAccess, smt::Expression::select(
@@ -1214,7 +1214,7 @@ smt::Expression SMTChecker::arithmeticOperation(
 	if (_op == Token::Div || _op == Token::Mod)
 	{
 		checkCondition(_right == 0, _location, "Division by zero", "<result>", &_right);
-		m_interface.addAssertion(_right != 0);
+		m_interface->addAssertion(_right != 0);
 	}
 
 	addOverflowTarget(
@@ -1396,7 +1396,7 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio
 		addOverflowTarget(OverflowTarget::Type::All, TypeProvider::uint(160), _value, _location);
 	else if (type->category() == Type::Category::Mapping)
 		arrayAssignment();
-	m_interface.addAssertion(m_context.newValue(_variable) == _value);
+	m_interface->addAssertion(m_context.newValue(_variable) == _value);
 }
 
 SMTChecker::VariableIndices SMTChecker::visitBranch(ASTNode const* _statement, smt::Expression _condition)
@@ -1425,7 +1425,7 @@ void SMTChecker::checkCondition(
 	smt::Expression const* _additionalValue
 )
 {
-	m_interface.push();
+	m_interface->push();
 	addPathConjoinedExpression(_condition);
 
 	vector<smt::Expression> expressionsToEvaluate;
@@ -1537,7 +1537,7 @@ void SMTChecker::checkCondition(
 		m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
 		break;
 	}
-	m_interface.pop();
+	m_interface->pop();
 }
 
 void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string const& _description)
@@ -1546,15 +1546,15 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
 	if (dynamic_cast<Literal const*>(&_condition))
 		return;
 
-	m_interface.push();
+	m_interface->push();
 	addPathConjoinedExpression(expr(_condition));
 	auto positiveResult = checkSatisfiable();
-	m_interface.pop();
+	m_interface->pop();
 
-	m_interface.push();
+	m_interface->push();
 	addPathConjoinedExpression(!expr(_condition));
 	auto negatedResult = checkSatisfiable();
-	m_interface.pop();
+	m_interface->pop();
 
 	if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
 		m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver.");
@@ -1599,7 +1599,7 @@ SMTChecker::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _exp
 	vector<string> values;
 	try
 	{
-		tie(result, values) = m_interface.check(_expressionsToEvaluate);
+		tie(result, values) = m_interface->check(_expressionsToEvaluate);
 	}
 	catch (smt::SolverError const& _e)
 	{
@@ -1635,7 +1635,7 @@ void SMTChecker::initializeFunctionCallParameters(CallableDeclaration const& _fu
 	for (unsigned i = 0; i < funParams.size(); ++i)
 		if (createVariable(*funParams[i]))
 		{
-			m_interface.addAssertion(_callArgs[i] == m_context.newValue(*funParams[i]));
+			m_interface->addAssertion(_callArgs[i] == m_context.newValue(*funParams[i]));
 			if (funParams[i]->annotation().type->category() == Type::Category::Mapping)
 				m_arrayAssignmentHappened = true;
 		}
@@ -1701,7 +1701,7 @@ void SMTChecker::mergeVariables(set<VariableDeclaration const*> const& _variable
 		int trueIndex = _indicesEndTrue.at(decl);
 		int falseIndex = _indicesEndFalse.at(decl);
 		solAssert(trueIndex != falseIndex, "");
-		m_interface.addAssertion(m_context.newValue(*decl) == smt::Expression::ite(
+		m_interface->addAssertion(m_context.newValue(*decl) == smt::Expression::ite(
 			_condition,
 			valueAtIndex(*decl, trueIndex),
 			valueAtIndex(*decl, falseIndex))
@@ -1761,7 +1761,7 @@ void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
 {
 	createExpr(_e);
 	solAssert(smt::smtKind(_e.annotation().type->category()) != smt::Kind::Function, "Equality operator applied to type that is not fully supported");
-	m_interface.addAssertion(expr(_e) == _value);
+	m_interface->addAssertion(expr(_e) == _value);
 }
 
 void SMTChecker::popPathCondition()
@@ -1810,12 +1810,12 @@ void SMTChecker::pushCallStack(CallStackEntry _entry)
 
 void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e)
 {
-	m_interface.addAssertion(currentPathConditions() && _e);
+	m_interface->addAssertion(currentPathConditions() && _e);
 }
 
 void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
 {
-	m_interface.addAssertion(smt::Expression::implies(currentPathConditions(), _e));
+	m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e));
 }
 
 bool SMTChecker::isRootFunction()
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 661dff342..c3e973528 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -53,7 +53,7 @@ public:
 	/// 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(); }
+	std::vector<std::string> unhandledQueries() { return m_interface->unhandledQueries(); }
 
 	/// @returns the FunctionDefinition of a called function if possible and should inline,
 	/// otherwise nullptr.
@@ -91,10 +91,6 @@ private:
 	void endVisit(IndexAccess const& _node) override;
 	bool visit(InlineAssembly const& _node) override;
 
-	smt::Expression assertions() { return m_interface.assertions(); }
-	void push() { m_interface.push(); }
-	void pop() { m_interface.pop(); }
-
 	/// Do not visit subtree if node is a RationalNumber.
 	/// Symbolic _expr is the rational literal.
 	bool shortcutRationalNumber(Expression const& _expr);
@@ -274,7 +270,7 @@ private:
 	/// @returns the VariableDeclaration referenced by an Identifier or nullptr.
 	VariableDeclaration const* identifierToVariable(Expression const& _expr);
 
-	smt::SMTPortfolio m_interface;
+	std::shared_ptr<smt::SolverInterface> m_interface;
 	smt::VariableUsage m_variableUsage;
 	bool m_loopExecutionHappened = false;
 	bool m_arrayAssignmentHappened = false;
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp
index ea2f3d9ee..09a311f4f 100644
--- a/libsolidity/formal/SMTPortfolio.cpp
+++ b/libsolidity/formal/SMTPortfolio.cpp
@@ -43,21 +43,18 @@ SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
 
 void SMTPortfolio::reset()
 {
-	m_assertions.clear();
 	for (auto const& s: m_solvers)
 		s->reset();
 }
 
 void SMTPortfolio::push()
 {
-	m_assertions.push_back(Expression(true));
 	for (auto const& s: m_solvers)
 		s->push();
 }
 
 void SMTPortfolio::pop()
 {
-	m_assertions.pop_back();
 	for (auto const& s: m_solvers)
 		s->pop();
 }
@@ -70,23 +67,10 @@ void SMTPortfolio::declareVariable(string const& _name, Sort const& _sort)
 
 void SMTPortfolio::addAssertion(Expression const& _expr)
 {
-	if (m_assertions.empty())
-		m_assertions.push_back(_expr);
-	else
-		m_assertions.back() = _expr && move(m_assertions.back());
-
 	for (auto const& s: m_solvers)
 		s->addAssertion(_expr);
 }
 
-Expression SMTPortfolio::assertions()
-{
-	if (m_assertions.empty())
-		return Expression(true);
-
-	return m_assertions.back();
-}
-
 /*
  * Broadcasts the SMT query to all solvers and returns a single result.
  * This comment explains how this result is decided.
diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h
index 1f61ead8d..3eb0a793b 100644
--- a/libsolidity/formal/SMTPortfolio.h
+++ b/libsolidity/formal/SMTPortfolio.h
@@ -53,8 +53,6 @@ public:
 
 	void addAssertion(Expression const& _expr) override;
 
-	Expression assertions();
-
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
 
 	std::vector<std::string> unhandledQueries() override;