division-by-zero on float

This disables the division-by-zero check for floating-point operations.
Division by zero on floating-point numbers is defined behavior when using
IEEE 754.

Author: kroening

Diff for: src/ansi-c/goto_check_c.cpp

@@ -1850,7 +1850,15 @@ void goto_check_ct::check_rec_div(
   const div_exprt &div_expr,
   const guardt &guard)
 {
-  div_by_zero_check(to_div_expr(div_expr), guard);
+  if(div_expr.type().id() == ID_signedbv ||
+     div_expr.type().id() == ID_unsignedbv ||
+     div_expr.type().id() == ID_c_bool)
+  {
+    // Division by zero is undefined behavior for all integer types.
+    // Division by zero is defined behavior for
+    // floating-point types if IEEE 754 is used.
+    div_by_zero_check(to_div_expr(div_expr), guard);
+  }
 
   if(div_expr.type().id() == ID_signedbv)
     integer_overflow_check(div_expr, guard);