From f5330c9fe44c8a290785b2ad206fe330112967f2 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 2 Mar 2018 08:14:44 +0000
Subject: [PATCH] Correct can_cast_expr for quantifier_exprt

---
 src/util/std_expr.h | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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<quantifier_exprt>(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,