Merge pull request #1901 from romainbrenguier/fix/quantifier_exprt

Daniel Kroening · web-flow · commit fdba57c45119 · 2018-03-05T21:31:48.000Z
Correct can_cast_expr for quantifier_exprt
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
@@ -4812,8 +4812,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
`@@ -4812,8 +4812,9 @@ inline quantifier_exprt &to_quantifier_expr(exprt &expr)`
`4812`	`4812`
`4813`	`4813`	`template<> inline bool can_cast_expr<quantifier_exprt>(const exprt &base)`
`4814`	`4814`	`{`
`4815`		`- return true;`
	`4815`	`+ return base.id() == ID_forall \|\| base.id() == ID_exists;`
`4816`	`4816`	`}`
	`4817`	`+`
`4817`	`4818`	`inline void validate_expr(const quantifier_exprt &value)`
`4818`	`4819`	`{`
`4819`	`4820`	`validate_operands(value, 2,`