diff options
| author | Leonardo Alt <leo@ethereum.org> | 2018-06-26 18:41:26 +0800 |
|---|---|---|
| committer | Alex Beregszaszi <alex@rtfs.hu> | 2018-07-27 23:16:26 +0800 |
| commit | 55c1fb60b4ba60685262f332f2b197a7ef81d5b8 (patch) | |
| tree | c861a097b885416b67d2ef98f20ae9f91950756d /libsolidity/formal/SMTChecker.cpp | |
| parent | 87a38e1abe61547e66aedfa595a73fb78184d609 (diff) | |
| download | dexon-solidity-55c1fb60b4ba60685262f332f2b197a7ef81d5b8.tar dexon-solidity-55c1fb60b4ba60685262f332f2b197a7ef81d5b8.tar.gz dexon-solidity-55c1fb60b4ba60685262f332f2b197a7ef81d5b8.tar.bz2 dexon-solidity-55c1fb60b4ba60685262f332f2b197a7ef81d5b8.tar.lz dexon-solidity-55c1fb60b4ba60685262f332f2b197a7ef81d5b8.tar.xz dexon-solidity-55c1fb60b4ba60685262f332f2b197a7ef81d5b8.tar.zst dexon-solidity-55c1fb60b4ba60685262f332f2b197a7ef81d5b8.zip | |
[SMTChecker] Add CheckResult::CONFLICTING
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 67625556..109c8dbe 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -617,6 +617,9 @@ void SMTChecker::checkCondition( case smt::CheckResult::UNKNOWN: m_errorReporter.warning(_location, _description + " might happen here." + loopComment); break; + case smt::CheckResult::CONFLICTING: + m_errorReporter.warning(_location, "At least two SMT solvers provided conflicting answers. Results might not be sound."); + break; case smt::CheckResult::ERROR: m_errorReporter.warning(_location, "Error trying to invoke SMT solver."); break; @@ -644,6 +647,8 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR) m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver."); + else if (positiveResult == smt::CheckResult::CONFLICTING || negatedResult == smt::CheckResult::CONFLICTING) + m_errorReporter.warning(_condition.location(), "At least two SMT solvers provided conflicting answers. Results might not be sound."); else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE) { // everything fine. |