Correct can_cast_expr for quantifier_exprt

romainbrenguier · romainbrenguier · commit f5330c9fe44c · 2018-03-02T08:30:35.000Z
diff --git 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,

Original file line number	Diff line number	Diff line change
`@@ -4804,8 +4804,9 @@ inline quantifier_exprt &to_quantifier_expr(exprt &expr)`
`4804`	`4804`
`4805`	`4805`	`template<> inline bool can_cast_expr<quantifier_exprt>(const exprt &base)`
`4806`	`4806`	`{`
`4807`		`- return true;`
	`4807`	`+ return base.id() == ID_forall \|\| base.id() == ID_exists;`
`4808`	`4808`	`}`
	`4809`	`+`
`4809`	`4810`	`inline void validate_expr(const quantifier_exprt &value)`
`4810`	`4811`	`{`
`4811`	`4812`	`validate_operands(value, 2,`