diff --git a/src/util/mathematical_expr.h b/src/util/mathematical_expr.h
index b4536737256..226aba5552a 100644
--- a/src/util/mathematical_expr.h
+++ b/src/util/mathematical_expr.h
@@ -337,6 +337,24 @@ class forall_exprt : public quantifier_exprt
   }
 };
 
+inline const forall_exprt &to_forall_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_forall);
+  DATA_INVARIANT(
+    expr.operands().size() == 2,
+    "forall expressions have exactly two operands");
+  return static_cast<const forall_exprt &>(expr);
+}
+
+inline forall_exprt &to_forall_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_forall);
+  DATA_INVARIANT(
+    expr.operands().size() == 2,
+    "forall expressions have exactly two operands");
+  return static_cast<forall_exprt &>(expr);
+}
+
 /// \brief An exists expression
 class exists_exprt : public quantifier_exprt
 {