From ae3350ae0320d140a427d2fa318e7002745a73a5 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leonardoaltt@gmail.com>
Date: Fri, 6 Apr 2018 18:01:40 +0200
Subject: [SMTChecker] Integration with CVC4

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

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

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 8f4abdc2..da6b632c 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -19,6 +19,8 @@
 
 #ifdef HAVE_Z3
 #include <libsolidity/formal/Z3Interface.h>
+#elif HAVE_CVC4
+#include <libsolidity/formal/CVC4Interface.h>
 #else
 #include <libsolidity/formal/SMTLib2Interface.h>
 #endif
@@ -39,6 +41,8 @@ using namespace dev::solidity;
 SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback):
 #ifdef HAVE_Z3
 	m_interface(make_shared<smt::Z3Interface>()),
+#elif HAVE_CVC4
+	m_interface(make_shared<smt::CVC4Interface>()),
 #else
 	m_interface(make_shared<smt::SMTLib2Interface>(_readFileCallback)),
 #endif
-- 
cgit v1.2.3