diff options
| author | Leonardo Alt <leo@ethereum.org> | 2018-08-03 23:04:56 +0800 |
|---|---|---|
| committer | Leonardo Alt <leo@ethereum.org> | 2018-11-23 16:43:49 +0800 |
| commit | f3c2309c736ffcdb84fc133106b05d1be1eda95a (patch) | |
| tree | f17d67ec037f7de5235da7df24a73e3406a52e62 /libsolidity/formal/SMTPortfolio.cpp | |
| parent | f44be616c96159fca18ad2f9ca4a1c0cb4218490 (diff) | |
| download | dexon-solidity-f3c2309c736ffcdb84fc133106b05d1be1eda95a.tar dexon-solidity-f3c2309c736ffcdb84fc133106b05d1be1eda95a.tar.gz dexon-solidity-f3c2309c736ffcdb84fc133106b05d1be1eda95a.tar.bz2 dexon-solidity-f3c2309c736ffcdb84fc133106b05d1be1eda95a.tar.lz dexon-solidity-f3c2309c736ffcdb84fc133106b05d1be1eda95a.tar.xz dexon-solidity-f3c2309c736ffcdb84fc133106b05d1be1eda95a.tar.zst dexon-solidity-f3c2309c736ffcdb84fc133106b05d1be1eda95a.zip | |
Display better error message in SMTLib2
Diffstat (limited to 'libsolidity/formal/SMTPortfolio.cpp')
| -rw-r--r-- | libsolidity/formal/SMTPortfolio.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp index 515d6f32..2c95c3fa 100644 --- a/libsolidity/formal/SMTPortfolio.cpp +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -45,8 +45,10 @@ SMTPortfolio::SMTPortfolio(map<h256, string> const& _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." + "SMT-LIB2 query responses were given in the auxiliary input, " + "but this Solidity binary uses an SMT solver (Z3/CVC4) directly." + "These responses will be ignored." + "Consider disabling Z3/CVC4 at compilation time in order to use SMT-LIB2 responses." ); #endif (void)_smtlib2Responses; |