diff options
| author | Leonardo Alt <leo@ethereum.org> | 2018-08-24 18:02:56 +0800 |
|---|---|---|
| committer | Leonardo Alt <leo@ethereum.org> | 2018-11-23 16:43:49 +0800 |
| commit | 6251a289dd55cc54f8da5a907dc4982a4b5e57fa (patch) | |
| tree | 88fa7520c103ada39f667c17467a516e59847793 /libsolidity/formal | |
| parent | dee0c4ded8636f2e8d157df79745ce907fa47c75 (diff) | |
| download | dexon-solidity-6251a289dd55cc54f8da5a907dc4982a4b5e57fa.tar.gz dexon-solidity-6251a289dd55cc54f8da5a907dc4982a4b5e57fa.tar.zst dexon-solidity-6251a289dd55cc54f8da5a907dc4982a4b5e57fa.zip | |
Testing with smtlib2 interface always there
Diffstat (limited to 'libsolidity/formal')
| -rw-r--r-- | libsolidity/formal/SMTPortfolio.cpp | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp index 6bdbd310..2a109b89 100644 --- a/libsolidity/formal/SMTPortfolio.cpp +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -23,9 +23,7 @@ #ifdef HAVE_CVC4 #include <libsolidity/formal/CVC4Interface.h> #endif -#if !defined (HAVE_Z3) && !defined (HAVE_CVC4) #include <libsolidity/formal/SMTLib2Interface.h> -#endif using namespace std; using namespace dev; @@ -34,16 +32,13 @@ using namespace dev::solidity::smt; SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses) { + m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses)); #ifdef HAVE_Z3 m_solvers.emplace_back(make_shared<smt::Z3Interface>()); #endif #ifdef HAVE_CVC4 m_solvers.emplace_back(make_shared<smt::CVC4Interface>()); #endif -#if !defined (HAVE_Z3) && !defined (HAVE_CVC4) - m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses)); -#endif - (void)_smtlib2Responses; } void SMTPortfolio::reset() |