Skip to content

Commit 1a417eb

Browse files
committed
add array_comprehension case to to_binding_expr
As identified in #6810, to_binding_expr could also cover array_comprehension expressions.
1 parent 8a885f0 commit 1a417eb

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

src/util/std_expr.h

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3090,7 +3090,8 @@ inline void validate_expr(const binding_exprt &binding_expr)
30903090
inline const binding_exprt &to_binding_expr(const exprt &expr)
30913091
{
30923092
PRECONDITION(
3093-
expr.id() == ID_forall || expr.id() == ID_exists || expr.id() == ID_lambda);
3093+
expr.id() == ID_forall || expr.id() == ID_exists ||
3094+
expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
30943095
const binding_exprt &ret = static_cast<const binding_exprt &>(expr);
30953096
validate_expr(ret);
30963097
return ret;
@@ -3105,7 +3106,8 @@ inline const binding_exprt &to_binding_expr(const exprt &expr)
31053106
inline binding_exprt &to_binding_expr(exprt &expr)
31063107
{
31073108
PRECONDITION(
3108-
expr.id() == ID_forall || expr.id() == ID_exists || expr.id() == ID_lambda);
3109+
expr.id() == ID_forall || expr.id() == ID_exists ||
3110+
expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
31093111
binding_exprt &ret = static_cast<binding_exprt &>(expr);
31103112
validate_expr(ret);
31113113
return ret;

0 commit comments

Comments
 (0)