Fix short circuit with assignments

This commit is contained in:
Leonardo Alt
2019-05-06 11:04:43 +02:00
parent befadea0c6
commit 80712f44cb
5 changed files with 86 additions and 3 deletions
+2 -3
View File
@@ -1230,17 +1230,16 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
{
// @TODO check that both of them are not constant
_op.leftExpression().accept(*this);
auto touchedVars = touchedVariables(_op.leftExpression());
if (_op.getOperator() == Token::And)
{
auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression()));
mergeVariables(touchedVars, !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
}
else
{
auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression()));
mergeVariables(touchedVars, expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
}
}