File tree Expand file tree Collapse file tree 1 file changed +4
-2
lines changed
Expand file tree Collapse file tree 1 file changed +4
-2
lines changed Original file line number Diff line number Diff line change @@ -3090,7 +3090,8 @@ inline void validate_expr(const binding_exprt &binding_expr)
30903090inline 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)
31053106inline 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;
You can’t perform that action at this time.
0 commit comments