cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Testing with smtlib2 interface always there

Browse Source
This commit is contained in:
Leonardo Alt 2018-08-24 12:02:56 +02:00
parent dee0c4ded8
commit 6251a289dd
1 changed files with 1 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
libsolidity/formal/SMTPortfolio.cpp
View File

@ -23,9 +23,7 @@
#ifdef HAVE_CVC4 #ifdef HAVE_CVC4
#include <libsolidity/formal/CVC4Interface.h> #include <libsolidity/formal/CVC4Interface.h>
#endif #endif
#if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
#include <libsolidity/formal/SMTLib2Interface.h> #include <libsolidity/formal/SMTLib2Interface.h>
#endif
using namespace std; using namespace std;
using namespace dev; using namespace dev;
@ -34,16 +32,13 @@ using namespace dev::solidity::smt;
SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses) SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
{ {
m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses));
#ifdef HAVE_Z3 #ifdef HAVE_Z3
m_solvers.emplace_back(make_shared<smt::Z3Interface>()); m_solvers.emplace_back(make_shared<smt::Z3Interface>());
#endif #endif
#ifdef HAVE_CVC4 #ifdef HAVE_CVC4
m_solvers.emplace_back(make_shared<smt::CVC4Interface>()); m_solvers.emplace_back(make_shared<smt::CVC4Interface>());
#endif #endif
#if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses));
#endif
(void)_smtlib2Responses;
} }
void SMTPortfolio::reset() void SMTPortfolio::reset()