cerc-io/solidity
10
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

Catch exception in Z3.

Browse Source 
Note: This exception might not be the result of resource limitation,
it might also hint towards usage error.
This commit is contained in:
chriseth 2017-10-11 15:15:17 +02:00 committed by Alex Beregszaszi
parent a71c6faf0f
commit 153ae98878
1 changed files with 28 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

47
libsolidity/formal/Z3Interface.cpp
View File

@ -73,28 +73,37 @@ void Z3Interface::addAssertion(Expression const& _expr)
pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _expressionsToEvaluate)
{
CheckResult result;
switch (m_solver.check())
vector<string> values;
try
{
case z3::check_result::sat:
result = CheckResult::SATISFIABLE;
break;
case z3::check_result::unsat:
result = CheckResult::UNSATISFIABLE;
break;
case z3::check_result::unknown:
result = CheckResult::UNKNOWN;
break;
default:
solAssert(false, "");
switch (m_solver.check())
{
case z3::check_result::sat:
result = CheckResult::SATISFIABLE;
break;
case z3::check_result::unsat:
result = CheckResult::UNSATISFIABLE;
break;
case z3::check_result::unknown:
result = CheckResult::UNKNOWN;
break;
default:
solAssert(false, "");
}
if (result != CheckResult::UNSATISFIABLE)
{
z3::model m = m_solver.get_model();
for (Expression const& e: _expressionsToEvaluate)
values.push_back(toString(m.eval(toZ3Expr(e))));
}
}
catch (z3::exception const& _e)
{
result = CheckResult::ERROR;
values.clear();
}
vector<string> values;
if (result != CheckResult::UNSATISFIABLE)
{
z3::model m = m_solver.get_model();
for (Expression const& e: _expressionsToEvaluate)
values.push_back(toString(m.eval(toZ3Expr(e))));
}
return make_pair(result, values);
}