diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1
index 581c859b7f8..f27bf308c17 100644
--- a/doc/man/cbmc.1
+++ b/doc/man/cbmc.1
@@ -62,7 +62,10 @@ enable array bounds checks
 check shift greater than bit\-width
 .TP
 \fB\-\-div\-by\-zero\-check\fR
-enable division by zero checks
+enable division by zero checks for integer division
+.TP
+\fB\-\-float\-div\-by\-zero\-check\fR
+enable division by zero checks for floating-point division
 .TP
 \fB\-\-pointer\-primitive\-check\fR
 checks that all pointers in pointer primitives are valid or null
diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1
index 9517eef3072..7db47a91086 100644
--- a/doc/man/goto-analyzer.1
+++ b/doc/man/goto-analyzer.1
@@ -521,7 +521,10 @@ Enable memory cleanup checks: assert that all dynamically allocated memory is
 explicitly freed before terminating the program.
 .TP
 \fB\-\-div\-by\-zero\-check\fR
-enable division by zero checks
+enable division by zero checks for integer division
+.TP
+\fB\-\-float\-div\-by\-zero\-check\fR
+enable division by zero checks for floating-point division
 .TP
 \fB\-\-signed\-overflow\-check\fR
 enable signed arithmetic over\- and underflow checks
diff --git a/doc/man/goto-diff.1 b/doc/man/goto-diff.1
index 5bb6318c6e4..6866cfdfd42 100644
--- a/doc/man/goto-diff.1
+++ b/doc/man/goto-diff.1
@@ -52,7 +52,10 @@ Enable memory cleanup checks: assert that all dynamically allocated memory is
 explicitly freed before terminating the program.
 .TP
 \fB\-\-div\-by\-zero\-check\fR
-enable division by zero checks
+enable division by zero checks for integer division
+.TP
+\fB\-\-float\-div\-by\-zero\-check\fR
+enable division by zero checks for floating-point division
 .TP
 \fB\-\-signed\-overflow\-check\fR
 enable signed arithmetic over\- and underflow checks
diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1
index 88428b58c7c..03141e2f55c 100644
--- a/doc/man/goto-instrument.1
+++ b/doc/man/goto-instrument.1
@@ -192,7 +192,10 @@ Enable memory cleanup checks: assert that all dynamically allocated memory is
 explicitly freed before terminating the program.
 .TP
 \fB\-\-div\-by\-zero\-check\fR
-enable division by zero checks
+enable division by zero checks for integer division
+.TP
+\fB\-\-float\-div\-by\-zero\-check\fR
+enable division by zero checks for floating-point division
 .TP
 \fB\-\-signed\-overflow\-check\fR
 enable signed arithmetic over\- and underflow checks
diff --git a/regression/cbmc/Division/floating_point_division1.c b/regression/cbmc/Division/floating_point_division1.c
new file mode 100644
index 00000000000..47dca33aac7
--- /dev/null
+++ b/regression/cbmc/Division/floating_point_division1.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  assert(1.0 / 2 == 0.5);
+  assert(1.0 / 0 == INFINITY);
+  assert(-1.0 / 0 == -INFINITY);
+  assert(isnan(NAN / 0));
+  assert(1.0 / INFINITY == 0);
+  assert(isnan(INFINITY / INFINITY));
+}
diff --git a/regression/cbmc/Division/floating_point_division1.desc b/regression/cbmc/Division/floating_point_division1.desc
new file mode 100644
index 00000000000..e3e95918ebd
--- /dev/null
+++ b/regression/cbmc/Division/floating_point_division1.desc
@@ -0,0 +1,8 @@
+CORE
+floating_point_division1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Division/floating_point_division2.c b/regression/cbmc/Division/floating_point_division2.c
new file mode 100644
index 00000000000..1ace5af3737
--- /dev/null
+++ b/regression/cbmc/Division/floating_point_division2.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+#include <math.h>
+
+double nondet_double();
+
+int main()
+{
+  double y = nondet_double();
+
+  if(y == 0)
+  {
+    // we expect to catch this with --float-div-by-zero-check
+    double x = 1.0 / y;
+  }
+}
diff --git a/regression/cbmc/Division/floating_point_division2.desc b/regression/cbmc/Division/floating_point_division2.desc
new file mode 100644
index 00000000000..bf2c9d17685
--- /dev/null
+++ b/regression/cbmc/Division/floating_point_division2.desc
@@ -0,0 +1,9 @@
+CORE no-new-smt
+floating_point_division2.c
+--float-div-by-zero-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.float-division-by-zero\.1\] line \d+ floating-point division by zero in 1\.0 / y: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc/pragma_cprover_enable_all/main.c b/regression/cbmc/pragma_cprover_enable_all/main.c
index 329b30f3a53..10c0c43f9a4 100644
--- a/regression/cbmc/pragma_cprover_enable_all/main.c
+++ b/regression/cbmc/pragma_cprover_enable_all/main.c
@@ -16,6 +16,7 @@ int main()
 #pragma CPROVER check disable "bounds"
 #pragma CPROVER check disable "pointer"
 #pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
 #pragma CPROVER check disable "enum-range"
 #pragma CPROVER check disable "signed-overflow"
 #pragma CPROVER check disable "unsigned-overflow"
@@ -36,7 +37,7 @@ int main()
     ABC e;
     bool readable;
     char i;
-    signed int j;
+    signed int j, k;
     readable = __CPROVER_r_ok(q, 1);
     q = p + 2000000000000;
     q = r;
@@ -45,14 +46,16 @@ int main()
     else
       den = 1.0;
     y = x / den;
+    j = 10 / 0;
     e = 10;
     i += 1;
-    j += 1;
+    k += 1;
   }
 #pragma CPROVER check push
 #pragma CPROVER check enable "bounds"
 #pragma CPROVER check enable "pointer"
 #pragma CPROVER check enable "div-by-zero"
+#pragma CPROVER check enable "float-div-by-zero"
 #pragma CPROVER check enable "enum-range"
 #pragma CPROVER check enable "signed-overflow"
 #pragma CPROVER check enable "unsigned-overflow"
@@ -73,7 +76,7 @@ int main()
     ABC e;
     bool readable;
     char i;
-    signed int j;
+    signed int j, k;
     readable = __CPROVER_r_ok(q, 1);
     q = p + 2000000000000;
     q = r;
@@ -82,9 +85,10 @@ int main()
     else
       den = 1.0;
     y = x / den;
+    j = 10 / 0;
     e = 10;
     i += 1;
-    j += 1;
+    k += 1;
   }
 #pragma CPROVER check pop
 #pragma CPROVER check pop
diff --git a/regression/cbmc/pragma_cprover_enable_all/test.desc b/regression/cbmc/pragma_cprover_enable_all/test.desc
index 36a44729a53..6db26a25cd0 100644
--- a/regression/cbmc/pragma_cprover_enable_all/test.desc
+++ b/regression/cbmc/pragma_cprover_enable_all/test.desc
@@ -1,27 +1,29 @@
 CORE no-new-smt
 main.c
---object-bits 8 --enum-range-check --unsigned-overflow-check --pointer-overflow-check --float-overflow-check --conversion-check --nan-check
-^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
-^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
-^\[main\.pointer_arithmetic\.\d+\] line 78 pointer arithmetic: pointer outside object bounds in p \+ (\(signed int\))?2000000000000(l|ll): FAILURE
-^\[main\.NaN\.\d+\] line 84 NaN on / in x / den: FAILURE
-^\[main\.division-by-zero\.\d+\] line 84 division by zero in x / den: FAILURE
-^\[main\.overflow\.\d+\] line 84 arithmetic overflow on floating-point division in x / den: FAILURE
-^\[main\.enum-range-check\.\d+\] line 85 enum range check in \(ABC\)10: FAILURE
-^\[main\.overflow\.\d+\] line 86 arithmetic overflow on signed (to unsigned )?type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE
-^\[main\.overflow\.\d+\] line 87 arithmetic overflow on signed \+ in j \+ 1: FAILURE
+--object-bits 8 --enum-range-check --div-by-zero-check --unsigned-overflow-check --pointer-overflow-check --float-overflow-check --float-div-by-zero-check --conversion-check --nan-check
+^\[main\.pointer_primitives\.\d+\] line 80 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main\.pointer_primitives\.\d+\] line 80 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main\.pointer_arithmetic\.\d+\] line 81 pointer arithmetic: pointer outside object bounds in p \+ (\(signed int\))?2000000000000(l|ll): FAILURE
+^\[main\.NaN\.\d+\] line 87 NaN on / in x / den: FAILURE
+^\[main\.float-division-by-zero\.\d+\] line 87 floating-point division by zero in x / den: FAILURE
+^\[main\.overflow\.\d+\] line 87 arithmetic overflow on floating-point division in x / den: FAILURE
+^\[main\.division-by-zero\.\d+\] line 88 division by zero in 10 / 0: FAILURE$
+^\[main\.enum-range-check\.\d+\] line 89 enum range check in \(ABC\)10: FAILURE
+^\[main\.overflow\.\d+\] line 90 arithmetic overflow on signed (to unsigned )?type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE
+^\[main\.overflow\.\d+\] line 91 arithmetic overflow on signed \+ in k \+ 1: FAILURE
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
-^\[main\.pointer_primitives\.\d+\] line 40 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
-^\[main\.pointer_primitives\.\d+\] line 40 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
-^\[main\.pointer_arithmetic\.\d+\] line 41 pointer arithmetic: pointer outside object bounds in p \+ .*2000000000000(l|ll): FAILURE
-^\[main\.NaN\.\d+\] line 47 NaN on / in x / den: FAILURE
-^\[main\.division-by-zero\.\d+\] line 47 division by zero in x / den: FAILURE
-^\[main\.overflow\.\d+\] line 47 arithmetic overflow on floating-point division in x / den: FAILURE
-^\[main\.enum-range-check\.\d+\] line 48 enum range check in \(ABC\)10: FAILURE
-^\[main\.overflow\.\d+\] line 49 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE
-^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed \+ in j \+ 1: FAILURE
+^\[main\.pointer_primitives\.\d+\] line 41 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main\.pointer_primitives\.\d+\] line 41 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
+^\[main\.pointer_arithmetic\.\d+\] line 42 pointer arithmetic: pointer outside object bounds in p \+ .*2000000000000(l|ll): FAILURE
+^\[main\.NaN\.\d+\] line 48 NaN on / in x / den: FAILURE
+^\[main\.float-division-by-zero\.\d+\] line 49 floating-point division by zero in x / den: FAILURE
+^\[main\.overflow\.\d+\] line 48 arithmetic overflow on floating-point division in x / den: FAILURE
+^\[main\.division-by-zero\.\d+\] line 48 division by zero in 10 / 0: FAILURE$
+^\[main\.enum-range-check\.\d+\] line 49 enum range check in \(ABC\)10: FAILURE
+^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE
+^\[main\.overflow\.\d+\] line 51 arithmetic overflow on signed \+ in k \+ 1: FAILURE
 --
 This test uses all possible named-checks to maximize coverage.
diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp
index 992d9af33e7..a05a6520a69 100644
--- a/src/ansi-c/goto_check_c.cpp
+++ b/src/ansi-c/goto_check_c.cpp
@@ -58,6 +58,8 @@ class goto_check_ct
     enable_memory_cleanup_check =
       _options.get_bool_option("memory-cleanup-check");
     enable_div_by_zero_check = _options.get_bool_option("div-by-zero-check");
+    enable_float_div_by_zero_check =
+      _options.get_bool_option("float-div-by-zero-check");
     enable_enum_range_check = _options.get_bool_option("enum-range-check");
     enable_signed_overflow_check =
       _options.get_bool_option("signed-overflow-check");
@@ -179,6 +181,7 @@ class goto_check_ct
   void bounds_check_index(const index_exprt &, const guardt &);
   void bounds_check_bit_count(const unary_exprt &, const guardt &);
   void div_by_zero_check(const div_exprt &, const guardt &);
+  void float_div_by_zero_check(const div_exprt &, const guardt &);
   void mod_by_zero_check(const mod_exprt &, const guardt &);
   void mod_overflow_check(const mod_exprt &, const guardt &);
   void enum_range_check(const exprt &, const guardt &);
@@ -262,6 +265,7 @@ class goto_check_ct
   bool enable_memory_leak_check;
   bool enable_memory_cleanup_check;
   bool enable_div_by_zero_check;
+  bool enable_float_div_by_zero_check;
   bool enable_enum_range_check;
   bool enable_signed_overflow_check;
   bool enable_unsigned_overflow_check;
@@ -282,6 +286,7 @@ class goto_check_ct
     {"memory-leak-check", &enable_memory_leak_check},
     {"memory-cleanup-check", &enable_memory_cleanup_check},
     {"div-by-zero-check", &enable_div_by_zero_check},
+    {"float-div-by-zero-check", &enable_float_div_by_zero_check},
     {"enum-range-check", &enable_enum_range_check},
     {"signed-overflow-check", &enable_signed_overflow_check},
     {"unsigned-overflow-check", &enable_unsigned_overflow_check},
@@ -508,6 +513,27 @@ void goto_check_ct::div_by_zero_check(
     guard);
 }
 
+void goto_check_ct::float_div_by_zero_check(
+  const div_exprt &expr,
+  const guardt &guard)
+{
+  if(!enable_float_div_by_zero_check)
+    return;
+
+  // add divison by zero subgoal
+
+  exprt zero = from_integer(0, expr.op1().type());
+  const notequal_exprt inequality(expr.op1(), std::move(zero));
+
+  add_guarded_property(
+    inequality,
+    "floating-point division by zero",
+    "float-division-by-zero",
+    expr.find_source_location(),
+    expr,
+    guard);
+}
+
 void goto_check_ct::enum_range_check(const exprt &expr, const guardt &guard)
 {
   if(!enable_enum_range_check)
@@ -1850,7 +1876,21 @@ 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.
+    div_by_zero_check(to_div_expr(div_expr), guard);
+  }
+  else if(div_expr.type().id() == ID_floatbv)
+  {
+    // Division by zero on floating-point numbers may be undefined behavior.
+    // Annex F of the ISO C21 suggests that implementations that
+    // define __STDC_IEC_559__ follow IEEE 754 semantics,
+    // which defines the outcome of division by zero.
+    float_div_by_zero_check(to_div_expr(div_expr), guard);
+  }
 
   if(div_expr.type().id() == ID_signedbv)
     integer_overflow_check(div_expr, guard);
diff --git a/src/ansi-c/goto_check_c.h b/src/ansi-c/goto_check_c.h
index 9fcf818241b..7447a6e68e0 100644
--- a/src/ansi-c/goto_check_c.h
+++ b/src/ansi-c/goto_check_c.h
@@ -39,7 +39,8 @@ void goto_check_c(
 
 #define OPT_GOTO_CHECK                                                         \
   "(bounds-check)(pointer-check)(memory-leak-check)(memory-cleanup-check)"     \
-  "(div-by-zero-check)(enum-range-check)"                                      \
+  "(div-by-zero-check)(float-div-by-zero-check)"                               \
+  "(enum-range-check)"                                                         \
   "(signed-overflow-check)(unsigned-overflow-check)"                           \
   "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
   "(float-overflow-check)(nan-check)(no-built-in-assertions)"                  \
@@ -61,7 +62,10 @@ void goto_check_c(
   " {y--no-pointer-check} \t disable pointer checks\n"                         \
   " {y--memory-leak-check} \t enable memory leak checks\n"                     \
   " {y--memory-cleanup-check} \t enable memory cleanup checks\n"               \
-  " {y--div-by-zero-check} \t enable division by zero checks (default on)\n"   \
+  " {y--div-by-zero-check} \t "                                                \
+  "enable division by zero checks on integers (default on)\n"                  \
+  " {y--float-div-by-zero-check} \t "                                          \
+  "enable division by zero checks on floating-point numbers (default off)\n"   \
   " {y--no-div-by-zero-check} \t disable division by zero checks\n"            \
   " {y--signed-overflow-check} \t "                                            \
   "enable signed arithmetic over- and underflow checks (default on)\n"         \
@@ -123,6 +127,7 @@ void goto_check_c(
   PARSE_OPTION_OVERRIDE(cmdline, options, "bounds-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "div-by-zero-check"); \
+  PARSE_OPTION_OVERRIDE(cmdline, options, "float-div-by-zero-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "signed-overflow-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "undefined-shift-check"); \
   PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-primitive-check"); \
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index efcf9fc4244..6d4fc796b24 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -221,7 +221,7 @@ int __isnormalf(float f)
 float __builtin_inff(void)
 {
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
 #pragma CPROVER check disable "float-overflow"
   return 1.0f / 0.0f;
 #pragma CPROVER check pop
@@ -232,7 +232,7 @@ float __builtin_inff(void)
 double __builtin_inf(void)
 {
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
 #pragma CPROVER check disable "float-overflow"
   return 1.0 / 0.0;
 #pragma CPROVER check pop
@@ -243,7 +243,7 @@ double __builtin_inf(void)
 long double __builtin_infl(void)
 {
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
 #pragma CPROVER check disable "float-overflow"
   return 1.0l / 0.0l;
 #pragma CPROVER check pop
@@ -289,7 +289,7 @@ int __builtin_isnanf(float f)
 float __builtin_huge_valf(void)
 {
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
 #pragma CPROVER check disable "float-overflow"
   return 1.0f / 0.0f;
 #pragma CPROVER check pop
@@ -300,7 +300,7 @@ float __builtin_huge_valf(void)
 double __builtin_huge_val(void)
 {
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
 #pragma CPROVER check disable "float-overflow"
   return 1.0 / 0.0;
 #pragma CPROVER check pop
@@ -311,7 +311,7 @@ double __builtin_huge_val(void)
 long double __builtin_huge_vall(void)
 {
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
 #pragma CPROVER check disable "float-overflow"
   return 1.0l / 0.0l;
 #pragma CPROVER check pop
@@ -622,7 +622,7 @@ double __builtin_nan(const char *str)
 __CPROVER_hide:;
   (void)*str;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
   return 0.0/0.0;
 #pragma CPROVER check pop
 }
@@ -635,7 +635,7 @@ float __builtin_nanf(const char *str)
 __CPROVER_hide:;
   (void)*str;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
   return 0.0f/0.0f;
 #pragma CPROVER check pop
 }
@@ -661,7 +661,7 @@ double nan(const char *str) {
  __CPROVER_hide:;
   (void)*str;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
   return 0.0/0.0;
 #pragma CPROVER check pop
 }
@@ -673,7 +673,7 @@ float nanf(const char *str) {
  __CPROVER_hide:;
   (void)*str;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
   return 0.0f/0.0f;
 #pragma CPROVER check pop
 }
@@ -685,7 +685,7 @@ long double nanl(const char *str) {
  __CPROVER_hide:;
   (void)*str;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
   return 0.0/0.0;
 #pragma CPROVER check pop
 }
@@ -716,7 +716,7 @@ float nextUpf(float f)
 __CPROVER_hide:;
   if (__CPROVER_isnanf(f))
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0f/0.0f;  // NaN
 #pragma CPROVER check pop
   else if (f == 0.0f)
@@ -768,7 +768,7 @@ double nextUp(double d)
 __CPROVER_hide:;
   if (__CPROVER_isnand(d))
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0/0.0;  // NaN
 #pragma CPROVER check pop
   else if (d == 0.0)
@@ -819,7 +819,7 @@ long double nextUpl(long double d)
 __CPROVER_hide:;
   if(__CPROVER_isnanld(d))
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0/0.0;  // NaN
 #pragma CPROVER check pop
   else if (d == 0.0)
@@ -889,7 +889,7 @@ float sqrtf(float f)
 
   if ( f < 0.0f )
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0f/0.0f; // NaN
 #pragma CPROVER check pop
   else if (__CPROVER_isinff(f) ||   // +Inf only
@@ -982,7 +982,7 @@ double sqrt(double d)
 
   if ( d < 0.0 )
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0/0.0; // NaN
 #pragma CPROVER check pop
   else if (__CPROVER_isinfd(d) ||   // +Inf only
@@ -1059,7 +1059,7 @@ long double sqrtl(long double d)
 
   if(d < 0.0l)
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0l/0.0l; // NaN
 #pragma CPROVER check pop
   else if (__CPROVER_isinfld(d) ||   // +Inf only
@@ -2791,7 +2791,7 @@ double log(double x)
   {
     errno = EDOM;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0 / 0.0;
 #pragma CPROVER check pop
   }
@@ -2859,7 +2859,7 @@ float logf(float x)
   {
     errno = EDOM;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0f / 0.0f;
 #pragma CPROVER check pop
   }
@@ -2928,7 +2928,7 @@ long double logl(long double x)
   {
     errno = EDOM;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0l / 0.0l;
 #pragma CPROVER check pop
   }
@@ -3002,7 +3002,7 @@ double log2(double x)
   {
     errno = EDOM;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0 / 0.0;
 #pragma CPROVER check pop
   }
@@ -3069,7 +3069,7 @@ float log2f(float x)
   {
     errno = EDOM;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0f / 0.0f;
 #pragma CPROVER check pop
   }
@@ -3137,7 +3137,7 @@ long double log2l(long double x)
   {
     errno = EDOM;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0l / 0.0l;
 #pragma CPROVER check pop
   }
@@ -3211,7 +3211,7 @@ double log10(double x)
   {
     errno = EDOM;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0 / 0.0;
 #pragma CPROVER check pop
   }
@@ -3281,7 +3281,7 @@ float log10f(float x)
   {
     errno = EDOM;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0f / 0.0f;
 #pragma CPROVER check pop
   }
@@ -3351,7 +3351,7 @@ long double log10l(long double x)
   {
     errno = EDOM;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0l / 0.0l;
 #pragma CPROVER check pop
   }
@@ -3415,7 +3415,7 @@ double pow(double x, double y)
   {
     errno = EDOM;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0 / 0.0;
 #pragma CPROVER check pop
   }
@@ -3487,7 +3487,7 @@ double pow(double x, double y)
   }
   else if(isnan(x) || isnan(y))
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0 / 0.0;
 #pragma CPROVER check pop
 
@@ -3563,7 +3563,7 @@ float powf(float x, float y)
   {
     errno = EDOM;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0f / 0.0f;
 #pragma CPROVER check pop
   }
@@ -3638,7 +3638,7 @@ float powf(float x, float y)
   }
   else if(isnanf(x) || isnanf(y))
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0f / 0.0f;
 #pragma CPROVER check pop
 
@@ -3708,7 +3708,7 @@ long double powl(long double x, long double y)
   {
     errno = EDOM;
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0l / 0.0l;
 #pragma CPROVER check pop
   }
@@ -3784,7 +3784,7 @@ long double powl(long double x, long double y)
   }
   else if(isnanl(x) || isnanl(y))
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0l / 0.0l;
 #pragma CPROVER check pop
 
@@ -3852,7 +3852,7 @@ double fma(double x, double y, double z)
 {
   // see man fma (https://linux.die.net/man/3/fma)
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
   if(isnan(x) || isnan(y))
     return 0.0 / 0.0;
   else if(
@@ -3904,7 +3904,7 @@ float fmaf(float x, float y, float z)
 {
   // see man fma (https://linux.die.net/man/3/fma)
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
   if(isnanf(x) || isnanf(y))
     return 0.0f / 0.0f;
   else if(
@@ -3961,7 +3961,7 @@ long double fmal(long double x, long double y, long double z)
 {
   // see man fma (https://linux.die.net/man/3/fma)
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
   if(isnanl(x) || isnanl(y))
     return 0.0l / 0.0l;
   else if(
@@ -4072,7 +4072,7 @@ double __builtin_powi(double x, int y)
   }
   else if(isnan(x))
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0 / 0.0;
 #pragma CPROVER check pop
 
@@ -4193,7 +4193,7 @@ float __builtin_powif(float x, int y)
   }
   else if(isnanf(x))
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0f / 0.0f;
 #pragma CPROVER check pop
 
@@ -4309,7 +4309,7 @@ long double __builtin_powil(long double x, int y)
   }
   else if(isnan(x))
 #pragma CPROVER check push
-#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-div-by-zero"
     return 0.0l / 0.0l;
 #pragma CPROVER check pop
 
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
index 9a97ff32626..6952daae3cf 100644
--- a/src/ansi-c/scanner.l
+++ b/src/ansi-c/scanner.l
@@ -255,7 +255,7 @@ string_lit      ("L"|"u"|"U"|"u8")?["]{s_char}*["]
 
 CPROVER_PREFIX  "__CPROVER_"
 
-arith_check     ("conversion"|"undefined-shift"|"nan"|"div-by-zero")
+arith_check     ("conversion"|"undefined-shift"|"nan"|"div-by-zero"|"float-div-by-zero")
 enum_check      "enum-range"
 pointer_primitive "pointer-primitive"
 memory_check    ("bounds"|"pointer"|"memory-leak")