diff options
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 5b7807f7..477568a0 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -889,6 +889,10 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co { // everything fine. } + else if (positiveResult == smt::CheckResult::UNKNOWN || negatedResult == smt::CheckResult::UNKNOWN) + { + // can't do anything. + } else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE) m_errorReporter.warning(_condition.location(), "Condition unreachable."); else |