diff options
| author | chriseth <chris@ethereum.org> | 2017-10-13 23:57:58 +0800 |
|---|---|---|
| committer | Leonardo Alt <leo@ethereum.org> | 2018-11-23 16:43:49 +0800 |
| commit | 54bed454f6e7a53f51ec7e9bda7805900a2c8472 (patch) | |
| tree | 87be069348deaac4cc526f227466adadec1d94de /libsolidity/formal | |
| parent | bb10be789c269927e593b41d37aa0637db68bbe1 (diff) | |
| download | dexon-solidity-54bed454f6e7a53f51ec7e9bda7805900a2c8472.tar.gz dexon-solidity-54bed454f6e7a53f51ec7e9bda7805900a2c8472.tar.zst dexon-solidity-54bed454f6e7a53f51ec7e9bda7805900a2c8472.zip | |
Rename function and warn if responses are supplied for Z3.
Diffstat (limited to 'libsolidity/formal')
| -rw-r--r-- | libsolidity/formal/SMTPortfolio.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp index 4c591380..515d6f32 100644 --- a/libsolidity/formal/SMTPortfolio.cpp +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -41,7 +41,13 @@ SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses) 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)), + m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses)); +#else + if (!_smtlib2Responses.empty()) + m_errorReporter.warning( + "Query responses for smtlib2 were given in the auxiliary input, " + "but this Solidity binary uses an SMT solver directly." + ); #endif (void)_smtlib2Responses; } |