aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
authorLeonardo Alt <leo@ethereum.org>2018-08-24 18:02:56 +0800
committerLeonardo Alt <leo@ethereum.org>2018-11-23 16:43:49 +0800
commit6251a289dd55cc54f8da5a907dc4982a4b5e57fa (patch)
tree88fa7520c103ada39f667c17467a516e59847793 /libsolidity
parentdee0c4ded8636f2e8d157df79745ce907fa47c75 (diff)
downloaddexon-solidity-6251a289dd55cc54f8da5a907dc4982a4b5e57fa.tar
dexon-solidity-6251a289dd55cc54f8da5a907dc4982a4b5e57fa.tar.gz
dexon-solidity-6251a289dd55cc54f8da5a907dc4982a4b5e57fa.tar.bz2
dexon-solidity-6251a289dd55cc54f8da5a907dc4982a4b5e57fa.tar.lz
dexon-solidity-6251a289dd55cc54f8da5a907dc4982a4b5e57fa.tar.xz
dexon-solidity-6251a289dd55cc54f8da5a907dc4982a4b5e57fa.tar.zst
dexon-solidity-6251a289dd55cc54f8da5a907dc4982a4b5e57fa.zip
Testing with smtlib2 interface always there
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/formal/SMTPortfolio.cpp7
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()