From 06dbcb3afea63a935afc492b926f6b434bb78fa4 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 27 Jul 2018 14:13:22 +0200 Subject: Only ask for a model if it's SAT --- libsolidity/formal/CVC4Interface.cpp | 2 +- libsolidity/formal/SMTLib2Interface.cpp | 2 +- libsolidity/formal/Z3Interface.cpp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) (limited to 'libsolidity/formal') diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp index c6f2771d..0cb70d2f 100644 --- a/libsolidity/formal/CVC4Interface.cpp +++ b/libsolidity/formal/CVC4Interface.cpp @@ -109,7 +109,7 @@ pair> CVC4Interface::check(vector const& solAssert(false, ""); } - if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty()) + if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) { for (Expression const& e: _expressionsToEvaluate) values.push_back(toString(m_solver.getValue(toCVC4Expr(e)))); diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index 0e00665a..00ac523f 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -112,7 +112,7 @@ pair> SMTLib2Interface::check(vector con result = CheckResult::ERROR; vector values; - if (result != CheckResult::UNSATISFIABLE && result != CheckResult::ERROR) + if (result == CheckResult::SATISFIABLE && result != CheckResult::ERROR) values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend()); return make_pair(result, values); } diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index 41943c92..7e0788b3 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -92,7 +92,7 @@ pair> Z3Interface::check(vector const& _ solAssert(false, ""); } - if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty()) + if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) { z3::model m = m_solver.get_model(); for (Expression const& e: _expressionsToEvaluate) -- cgit v1.2.3