diff --git a/src/util/std_expr.h b/src/util/std_expr.h index cc04bd376f4..0215beaa2bb 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -4804,8 +4804,9 @@ inline quantifier_exprt &to_quantifier_expr(exprt &expr) template<> inline bool can_cast_expr(const exprt &base) { - return true; + return base.id() == ID_forall || base.id() == ID_exists; } + inline void validate_expr(const quantifier_exprt &value) { validate_operands(value, 2,