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 bcd1af1 commit cb9dbc4Copy full SHA for cb9dbc4
src/util/simplify_expr_boolean.cpp
@@ -27,17 +27,18 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
27
28
if(expr.id()==ID_implies)
29
{
30
+ const auto &implies_expr = to_implies_expr(expr);
31
+
32
if(
- expr.operands().size() != 2 ||
- expr.operands().front().type().id() != ID_bool ||
33
- expr.operands().back().type().id() != ID_bool)
+ implies_expr.op0().type().id() != ID_bool ||
34
+ implies_expr.op1().type().id() != ID_bool)
35
36
return unchanged(expr);
37
}
38
39
// turn a => b into !a || b
40
- auto new_expr = expr;
41
+ binary_exprt new_expr = implies_expr;
42
new_expr.id(ID_or);
43
new_expr.op0() = boolean_negate(new_expr.op0());
44
simplify_node(new_expr);
0 commit comments