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

Error message stays in the SMTChecker

Browse Source
This commit is contained in:
Leonardo Alt 2018-08-14 12:34:53 +02:00
parent f3c2309c73
commit dee0c4ded8
2 changed files with 9 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
libsolidity/formal/SMTChecker.cpp
View File

@ -36,6 +36,15 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _
m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses)),
m_errorReporter(_errorReporter)
{
#if defined (HAVE_Z3) || defined (HAVE_CVC4)
if (!_smtlib2Responses.empty())
m_errorReporter.warning(
"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 SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)

8
libsolidity/formal/SMTPortfolio.cpp
View File

@ -42,14 +42,6 @@ SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
#endif
#if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses));
#else
if (!_smtlib2Responses.empty())
m_errorReporter.warning(
"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;
}