diff options
Diffstat (limited to 'libsolidity')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 5 | ||||
| -rw-r--r-- | libsolidity/formal/SMTPortfolio.cpp | 7 | ||||
| -rw-r--r-- | libsolidity/formal/SolverInterface.h | 2 |
3 files changed, 10 insertions, 4 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. diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp index 25795738..64806097 100644 --- a/libsolidity/formal/SMTPortfolio.cpp +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -92,7 +92,7 @@ void SMTPortfolio::addAssertion(Expression const& _expr) * This comment explains how this result is decided. * * When a solver is queried, there are four possible answers: - * SATISFIABLE (SAT), UNSATISFIABLE (UNSAT), UNKNOWN, ERROR + * SATISFIABLE (SAT), UNSATISFIABLE (UNSAT), UNKNOWN, CONFLICTING, ERROR * We say that a solver _answered_ the query if it returns either: * SAT or UNSAT * A solver did not answer the query if it returns either: @@ -107,7 +107,7 @@ void SMTPortfolio::addAssertion(Expression const& _expr) * because one buggy solver/integration shouldn't break the portfolio. * * 2) If at least one solver answers SAT and at least one answers UNSAT, at least one of them is buggy - * and the result is conflicting and we abort. + * and the result is CONFLICTING. * In the future if we have more than 2 solvers enabled we could go with the majority. * * 3) If NO solver answers the query: @@ -135,7 +135,8 @@ pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const& } else if (lastResult != result) { - solAssert(false, "At least two SMT solvers gave opposing results."); + lastResult = CheckResult::CONFLICTING; + break; } } else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR) diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index f8a2bebb..8bbd0417 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -39,7 +39,7 @@ namespace smt enum class CheckResult { - SATISFIABLE, UNSATISFIABLE, UNKNOWN, ERROR + SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR }; enum class Sort |