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

Merge pull request #4599 from ethereum/smt_sat_model

Browse Source 
SMTChecker: Only ask for a model if it's SAT
This commit is contained in:
Alex Beregszaszi 2018-07-27 13:56:30 +01:00 committed by GitHub
commit c633ebe2e6
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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, "");
}
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))));

2
libsolidity/formal/SMTLib2Interface.cpp
View File

@ -112,7 +112,7 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con
result = CheckResult::ERROR;
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());
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, "");
}
if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty())
if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty())
{
z3::model m = m_solver.get_model();
for (Expression const& e: _expressionsToEvaluate)