isinf, isnan, isnormal require floatbv operands

Fail early if simplification encounters non-floatbv operands to these
functions. This would have been caught by ieee_floatt::from_expr, but
failing early makes diagnosing easier.

Author: tautschnig

src/util/simplify_expr_floatbv.cpp

@@ -20,6 +20,8 @@ Author: Daniel Kroening, [email protected]
 simplify_exprt::resultt<>
 simplify_exprt::simplify_isinf(const unary_exprt &expr)
 {
+  PRECONDITION(expr.op().type().id() == ID_floatbv);
+
   if(expr.op().is_constant())
   {
     ieee_floatt value(to_constant_expr(expr.op()));
@@ -32,6 +34,8 @@ simplify_exprt::simplify_isinf(const unary_exprt &expr)
 simplify_exprt::resultt<>
 simplify_exprt::simplify_isnan(const unary_exprt &expr)
 {
+  PRECONDITION(expr.op().type().id() == ID_floatbv);
+
   if(expr.op().is_constant())
   {
     ieee_floatt value(to_constant_expr(expr.op()));
@@ -44,6 +48,8 @@ simplify_exprt::simplify_isnan(const unary_exprt &expr)
 simplify_exprt::resultt<>
 simplify_exprt::simplify_isnormal(const unary_exprt &expr)
 {
+  PRECONDITION(expr.op().type().id() == ID_floatbv);
+
   if(expr.op().is_constant())
   {
     ieee_floatt value(to_constant_expr(expr.op()));