diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index a691e2e9f..78812dc7c 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -28,8 +28,9 @@ using namespace langutil;
 using namespace dev::solidity;
 
 BMC::BMC(smt::EncodingContext& _context, ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
-	SMTEncoder(_context, _smtlib2Responses),
-	m_outerErrorReporter(_errorReporter)
+	SMTEncoder(_context),
+	m_outerErrorReporter(_errorReporter),
+	m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses))
 {
 #if defined (HAVE_Z3) || defined (HAVE_CVC4)
 	if (!_smtlib2Responses.empty())
diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h
index d25cc5fdc..28ea2117e 100644
--- a/libsolidity/formal/BMC.h
+++ b/libsolidity/formal/BMC.h
@@ -30,7 +30,7 @@
 
 #include <libsolidity/formal/EncodingContext.h>
 #include <libsolidity/formal/SMTEncoder.h>
-#include <libsolidity/formal/SMTPortfolio.h>
+#include <libsolidity/formal/SolverInterface.h>
 
 #include <libsolidity/interface/ReadFile.h>
 #include <liblangutil/ErrorReporter.h>
@@ -174,6 +174,8 @@ private:
 	langutil::ErrorReporter& m_outerErrorReporter;
 
 	std::vector<VerificationTarget> m_verificationTargets;
+
+	std::shared_ptr<smt::SolverInterface> m_interface;
 };
 
 }
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 30aa95226..1cdbf2885 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -28,8 +28,7 @@ using namespace dev;
 using namespace langutil;
 using namespace dev::solidity;
 
-SMTEncoder::SMTEncoder(smt::EncodingContext& _context, map<h256, string> const& _smtlib2Responses):
-	m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses)),
+SMTEncoder::SMTEncoder(smt::EncodingContext& _context):
 	m_errorReporter(m_smtErrors),
 	m_context(_context)
 {
@@ -471,7 +470,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 		solAssert(value, "");
 
 		smt::Expression thisBalance = m_context.balance();
-		setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), *m_interface);
+		setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), *m_context.solver());
 
 		m_context.transfer(m_context.thisAddress(), expr(address), expr(*value));
 		break;
@@ -616,7 +615,7 @@ void SMTEncoder::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_context.solver());
 			m_context.createExpression(_literal, result.second);
 		}
 		m_errorReporter.warning(
@@ -686,7 +685,7 @@ bool SMTEncoder::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_context.solver());
 			m_uninterpretedTerms.insert(&_memberAccess);
 			return false;
 		}
@@ -733,7 +732,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 	setSymbolicUnknownValue(
 		expr(_indexAccess),
 		_indexAccess.annotation().type,
-		*m_interface
+		*m_context.solver()
 	);
 	m_uninterpretedTerms.insert(&_indexAccess);
 }
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 064a3a436..60dd67bb7 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -24,7 +24,6 @@
 
 
 #include <libsolidity/formal/EncodingContext.h>
-#include <libsolidity/formal/SMTPortfolio.h>
 #include <libsolidity/formal/SymbolicVariables.h>
 #include <libsolidity/formal/VariableUsage.h>
 
@@ -51,7 +50,7 @@ namespace solidity
 class SMTEncoder: public ASTConstVisitor
 {
 public:
-	SMTEncoder(smt::EncodingContext& _context, std::map<h256, std::string> const& _smtlib2Responses);
+	SMTEncoder(smt::EncodingContext& _context);
 
 	/// @returns the leftmost identifier in a multi-d IndexAccess.
 	static Expression const* leftmostBase(IndexAccess const& _indexAccess);
@@ -208,7 +207,6 @@ protected:
 	/// @returns a note to be added to warnings.
 	std::string extraComment();
 
-	std::shared_ptr<smt::SolverInterface> m_interface;
 	smt::VariableUsage m_variableUsage;
 	bool m_arrayAssignmentHappened = false;
 	// True if the "No SMT solver available" warning was already created.