diff options
| author | Leonardo Alt <leonardoaltt@gmail.com> | 2018-04-07 00:01:40 +0800 |
|---|---|---|
| committer | Alex Beregszaszi <alex@rtfs.hu> | 2018-04-17 19:26:58 +0800 |
| commit | ae3350ae0320d140a427d2fa318e7002745a73a5 (patch) | |
| tree | e4da5e3619baa56b09509004c58b1b5d12594e48 /libsolidity/formal/SMTChecker.cpp | |
| parent | 842fd0cd2cef3c11c392b7820e178fd0d034fa07 (diff) | |
| download | dexon-solidity-ae3350ae0320d140a427d2fa318e7002745a73a5.tar.gz dexon-solidity-ae3350ae0320d140a427d2fa318e7002745a73a5.tar.zst dexon-solidity-ae3350ae0320d140a427d2fa318e7002745a73a5.zip | |
[SMTChecker] Integration with CVC4
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 4 |
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 |