add non-const to_binding_expr

This adds a non-const variant of to_binding_expr.

Author: kroening

src/util/std_expr.h

@@ -3096,6 +3096,21 @@ inline const binding_exprt &to_binding_expr(const exprt &expr)
   return ret;
 }
 
+/// \brief Cast an exprt to a \ref binding_exprt
+///
+/// \a expr must be known to be \ref binding_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref binding_exprt
+inline binding_exprt &to_binding_expr(exprt &expr)
+{
+  PRECONDITION(
+    expr.id() == ID_forall || expr.id() == ID_exists || expr.id() == ID_lambda);
+  binding_exprt &ret = static_cast<binding_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 /// \brief A let expression
 class let_exprt : public binary_exprt
 {