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

Only ask for a model if it's SAT

Browse Source
This commit is contained in:
Leonardo Alt 2018-07-27 14:13:22 +02:00
parent bc51b0f6c2
commit 06dbcb3afe
3 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/CVC4Interface.cpp
View File

@ -109,7 +109,7 @@ pair<CheckResult, vector<string>> CVC4Interface::check(vector<Expression> const&
solAssert(false, ""); solAssert(false, "");
} }
if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty()) if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty())
{ {
for (Expression const& e: _expressionsToEvaluate) for (Expression const& e: _expressionsToEvaluate)
values.push_back(toString(m_solver.getValue(toCVC4Expr(e)))); values.push_back(toString(m_solver.getValue(toCVC4Expr(e))));

2
libsolidity/formal/SMTLib2Interface.cpp
View File

@ -112,7 +112,7 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con
result = CheckResult::ERROR; result = CheckResult::ERROR;
vector<string> values; vector<string> 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()); values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend());
return make_pair(result, values); return make_pair(result, values);
} }

2
libsolidity/formal/Z3Interface.cpp
View File

@ -92,7 +92,7 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
solAssert(false, ""); solAssert(false, "");
} }
if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty()) if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty())
{ {
z3::model m = m_solver.get_model(); z3::model m = m_solver.get_model();
for (Expression const& e: _expressionsToEvaluate) for (Expression const& e: _expressionsToEvaluate)