From 4cea3d4aa44194e052520fea2f6d216675d3bd14 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Thu, 13 Jul 2017 18:22:51 +0200
Subject: Insert abstraction layer.

---
 libsolidity/formal/SMTChecker.h | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'libsolidity/formal/SMTChecker.h')

diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 8c6a2327..afe5897d 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -18,7 +18,7 @@
 #pragma once
 
 #include <libsolidity/ast/ASTVisitor.h>
-#include <libsolidity/formal/SMTLib2Interface.h>
+#include <libsolidity/formal/SolverInterface.h>
 #include <libsolidity/interface/ReadFile.h>
 
 #include <map>
@@ -85,7 +85,7 @@ private:
 	/// The function takes one argument which is the "sequence number".
 	smt::Expression var(Declaration const& _decl);
 
-	smt::SMTLib2Interface m_interface;
+	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::map<Declaration const*, int> m_currentSequenceCounter;
 	std::map<Expression const*, smt::Expression> m_z3Expressions;
 	std::map<Declaration const*, smt::Expression> m_z3Variables;
-- 
cgit