mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Fix ite
This commit is contained in:
parent
2108580df6
commit
1efa03201d
@ -433,8 +433,8 @@ optional<LinearExpression> BooleanLPSolver::parseLinearSum(smtutil::Expression c
|
|||||||
else if (_expr.name == "ite")
|
else if (_expr.name == "ite")
|
||||||
{
|
{
|
||||||
Expression result = declareInternalVariable(false);
|
Expression result = declareInternalVariable(false);
|
||||||
addAssertion(_expr.arguments.at(0) || (result == _expr.arguments.at(1)));
|
addAssertion(!_expr.arguments.at(0) || (result == _expr.arguments.at(1)));
|
||||||
addAssertion(!_expr.arguments.at(0) || (result == _expr.arguments.at(2)));
|
addAssertion(_expr.arguments.at(0) || (result == _expr.arguments.at(2)));
|
||||||
return parseLinearSum(result);
|
return parseLinearSum(result);
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
Loading…
Reference in New Issue
Block a user