aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTChecker.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
-rw-r--r--libsolidity/formal/SMTChecker.cpp4
1 files changed, 4 insertions, 0 deletions
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