We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 27b0fda commit f3bf107Copy full SHA for f3bf107
src/util/simplify_expr_boolean.cpp
@@ -27,17 +27,17 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
27
28
if(expr.id()==ID_implies)
29
{
30
- if(
31
- expr.operands().size() != 2 ||
32
- expr.operands().front().type().id() != ID_bool ||
33
- expr.operands().back().type().id() != ID_bool)
+ const auto &implies_expr = to_implies_expr(expr);
+
+ if(implies_expr.op0().type().id() != ID_bool ||
+ implies_expr.op1().type().id() != ID_bool)
34
35
return unchanged(expr);
36
}
37
38
// turn a => b into !a || b
39
40
- auto new_expr = expr;
+ binary_exprt new_expr = implies_expr;
41
new_expr.id(ID_or);
42
new_expr.op0() = boolean_negate(new_expr.op0());
43
simplify_node(new_expr);
0 commit comments