From a2a8db46d39eb2da8af77ce73b2177277a6b3540 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 4 Jul 2025 19:35:32 +0000
Subject: [PATCH 1/2] Math library models: add missing *BSD variants, cleanup

BSD systems appear to use `__` prefixed variants of several functions.
Define these as needed. Also, avoid handling some GCC-style
`__builtin_`-prefixed functions via models when others are done directly
in the type checker: do all of them in the type checker.

In addition to `__builtin_isfinite`, recognise its older glibc
internal aliases `__builtin_finite`, `__builtin_finitef` and
`__builtin_finitel` in the same isfinite_exprt branch of the type
checker.  Some glibc `<bits/mathcalls-helper-functions.h>` headers
expose the legacy `finite()` API via these builtins, and without
recognition CBMC would otherwise treat them as body-less functions
returning nondet.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 regression/cbmc-library/__builtin_fabs/main.c |   9 --
 .../cbmc-library/__builtin_fabs/test.desc     |   8 --
 .../cbmc-library/__builtin_fabsf/main.c       |   9 --
 .../cbmc-library/__builtin_fabsf/test.desc    |   8 --
 .../cbmc-library/__builtin_fabsl/main.c       |   9 --
 .../cbmc-library/__builtin_fabsl/test.desc    |   8 --
 regression/cbmc-library/__fpclassify/main.c   |  29 ++++
 regression/cbmc-library/__isinf/main.c        |   9 --
 regression/cbmc-library/__isinf/test.desc     |   8 --
 regression/cbmc-library/__isinff/main.c       |   9 --
 regression/cbmc-library/__isinff/test.desc    |   8 --
 regression/cbmc-library/__isinfl/main.c       |   9 --
 regression/cbmc-library/__isinfl/test.desc    |   8 --
 regression/cbmc-library/__isnan/main.c        |   9 --
 regression/cbmc-library/__isnan/test.desc     |   8 --
 regression/cbmc-library/__isnanf/main.c       |   9 --
 regression/cbmc-library/__isnanf/test.desc    |   8 --
 regression/cbmc-library/__isnanl/main.c       |   9 --
 regression/cbmc-library/__isnanl/test.desc    |   8 --
 regression/cbmc-library/__isnormalf/main.c    |   9 --
 regression/cbmc-library/__isnormalf/test.desc |   8 --
 regression/cbmc-library/__signbit/main.c      |   9 --
 regression/cbmc-library/__signbit/test.desc   |   8 --
 regression/cbmc-library/__signbitf/main.c     |   9 --
 regression/cbmc-library/__signbitf/test.desc  |   8 --
 regression/cbmc-library/isfinite/main.c       |  15 +-
 regression/cbmc-library/isfinite/test.desc    |   4 +-
 regression/cbmc-library/isinf/main.c          |  16 +++
 regression/cbmc-library/isinff/main.c         |   9 --
 regression/cbmc-library/isinff/test.desc      |   8 --
 regression/cbmc-library/isinfl/main.c         |   9 --
 regression/cbmc-library/isinfl/test.desc      |   8 --
 regression/cbmc-library/isnanf/main.c         |   9 --
 regression/cbmc-library/isnanf/test.desc      |   8 --
 regression/cbmc-library/isnanl/main.c         |   9 --
 regression/cbmc-library/isnanl/test.desc      |   8 --
 regression/cbmc-library/isnormal/main.c       |   7 +-
 regression/cbmc-library/isnormal/test.desc    |   4 +-
 regression/cbmc-library/signbit/main.c        |   7 +
 src/ansi-c/c_typecheck_expr.cpp               |  30 ++--
 src/ansi-c/library/math.c                     | 131 ++++++++++--------
 src/ansi-c/library_check.sh                   |   7 +
 42 files changed, 173 insertions(+), 349 deletions(-)
 delete mode 100644 regression/cbmc-library/__builtin_fabs/main.c
 delete mode 100644 regression/cbmc-library/__builtin_fabs/test.desc
 delete mode 100644 regression/cbmc-library/__builtin_fabsf/main.c
 delete mode 100644 regression/cbmc-library/__builtin_fabsf/test.desc
 delete mode 100644 regression/cbmc-library/__builtin_fabsl/main.c
 delete mode 100644 regression/cbmc-library/__builtin_fabsl/test.desc
 delete mode 100644 regression/cbmc-library/__isinf/main.c
 delete mode 100644 regression/cbmc-library/__isinf/test.desc
 delete mode 100644 regression/cbmc-library/__isinff/main.c
 delete mode 100644 regression/cbmc-library/__isinff/test.desc
 delete mode 100644 regression/cbmc-library/__isinfl/main.c
 delete mode 100644 regression/cbmc-library/__isinfl/test.desc
 delete mode 100644 regression/cbmc-library/__isnan/main.c
 delete mode 100644 regression/cbmc-library/__isnan/test.desc
 delete mode 100644 regression/cbmc-library/__isnanf/main.c
 delete mode 100644 regression/cbmc-library/__isnanf/test.desc
 delete mode 100644 regression/cbmc-library/__isnanl/main.c
 delete mode 100644 regression/cbmc-library/__isnanl/test.desc
 delete mode 100644 regression/cbmc-library/__isnormalf/main.c
 delete mode 100644 regression/cbmc-library/__isnormalf/test.desc
 delete mode 100644 regression/cbmc-library/__signbit/main.c
 delete mode 100644 regression/cbmc-library/__signbit/test.desc
 delete mode 100644 regression/cbmc-library/__signbitf/main.c
 delete mode 100644 regression/cbmc-library/__signbitf/test.desc
 delete mode 100644 regression/cbmc-library/isinff/main.c
 delete mode 100644 regression/cbmc-library/isinff/test.desc
 delete mode 100644 regression/cbmc-library/isinfl/main.c
 delete mode 100644 regression/cbmc-library/isinfl/test.desc
 delete mode 100644 regression/cbmc-library/isnanf/main.c
 delete mode 100644 regression/cbmc-library/isnanf/test.desc
 delete mode 100644 regression/cbmc-library/isnanl/main.c
 delete mode 100644 regression/cbmc-library/isnanl/test.desc

diff --git a/regression/cbmc-library/__builtin_fabs/main.c b/regression/cbmc-library/__builtin_fabs/main.c
deleted file mode 100644
index 38b521fe15c..00000000000
--- a/regression/cbmc-library/__builtin_fabs/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_fabs();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_fabs/test.desc b/regression/cbmc-library/__builtin_fabs/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_fabs/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__builtin_fabsf/main.c b/regression/cbmc-library/__builtin_fabsf/main.c
deleted file mode 100644
index 7c4cc5cc1fd..00000000000
--- a/regression/cbmc-library/__builtin_fabsf/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_fabsf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_fabsf/test.desc b/regression/cbmc-library/__builtin_fabsf/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_fabsf/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__builtin_fabsl/main.c b/regression/cbmc-library/__builtin_fabsl/main.c
deleted file mode 100644
index 6e69656f497..00000000000
--- a/regression/cbmc-library/__builtin_fabsl/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_fabsl();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_fabsl/test.desc b/regression/cbmc-library/__builtin_fabsl/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_fabsl/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__fpclassify/main.c b/regression/cbmc-library/__fpclassify/main.c
index 8b05699e4a6..fbbeffb63a6 100644
--- a/regression/cbmc-library/__fpclassify/main.c
+++ b/regression/cbmc-library/__fpclassify/main.c
@@ -1,4 +1,5 @@
 #include <assert.h>
+#include <float.h>
 #include <math.h>
 
 #ifdef __GNUC__
@@ -49,5 +50,33 @@ int main(void)
   simplifiedInductiveStepHunt(g);
 #endif
 
+// Visual Studio needs to be 2013 onwards
+#if defined(_MSC_VER) && !defined(__CYGWIN__) && _MSC_VER < 1800
+
+  // see http://www.johndcook.com/math_h.html
+
+#else
+  assert(fpclassify(DBL_MAX + DBL_MAX) == FP_INFINITE);
+  assert(fpclassify(0 * (DBL_MAX + DBL_MAX)) == FP_NAN);
+  assert(fpclassify(1.0) == FP_NORMAL);
+  assert(fpclassify(DBL_MIN) == FP_NORMAL);
+  assert(fpclassify(DBL_MIN / 2) == FP_SUBNORMAL);
+  assert(fpclassify(-0.0) == FP_ZERO);
+#endif
+
+#if !defined(__clang__) && defined(__GNUC__)
+  assert(__builtin_fpclassify(0, 1, 2, 3, 4, DBL_MAX + DBL_MAX) == 1);
+  assert(__builtin_fpclassify(0, 1, 2, 3, 4, 0 * (DBL_MAX + DBL_MAX)) == 0);
+  assert(__builtin_fpclassify(0, 1, 2, 3, 4, 1.0) == 2);
+  assert(__builtin_fpclassify(0, 1, 2, 3, 4, DBL_MIN) == 2);
+  assert(__builtin_fpclassify(0, 1, 2, 3, 4, DBL_MIN / 2) == 3);
+  assert(__builtin_fpclassify(0, 1, 2, 3, 4, -0.0) == 4);
+
+  // these are compile-time
+  _Static_assert(
+    __builtin_fpclassify(0, 1, 2, 3, 4, -0.0) == 4,
+    "__builtin_fpclassify is constant");
+#endif
+
   return 0;
 }
diff --git a/regression/cbmc-library/__isinf/main.c b/regression/cbmc-library/__isinf/main.c
deleted file mode 100644
index 3441084533d..00000000000
--- a/regression/cbmc-library/__isinf/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __isinf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__isinf/test.desc b/regression/cbmc-library/__isinf/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isinf/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__isinff/main.c b/regression/cbmc-library/__isinff/main.c
deleted file mode 100644
index 446e25a9512..00000000000
--- a/regression/cbmc-library/__isinff/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __isinff();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__isinff/test.desc b/regression/cbmc-library/__isinff/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isinff/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__isinfl/main.c b/regression/cbmc-library/__isinfl/main.c
deleted file mode 100644
index df21c681f43..00000000000
--- a/regression/cbmc-library/__isinfl/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __isinfl();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__isinfl/test.desc b/regression/cbmc-library/__isinfl/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isinfl/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__isnan/main.c b/regression/cbmc-library/__isnan/main.c
deleted file mode 100644
index 3bd8ba542ca..00000000000
--- a/regression/cbmc-library/__isnan/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __isnan();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__isnan/test.desc b/regression/cbmc-library/__isnan/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isnan/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__isnanf/main.c b/regression/cbmc-library/__isnanf/main.c
deleted file mode 100644
index 074fea3bf29..00000000000
--- a/regression/cbmc-library/__isnanf/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __isnanf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__isnanf/test.desc b/regression/cbmc-library/__isnanf/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isnanf/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__isnanl/main.c b/regression/cbmc-library/__isnanl/main.c
deleted file mode 100644
index bdda6af323e..00000000000
--- a/regression/cbmc-library/__isnanl/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __isnanl();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__isnanl/test.desc b/regression/cbmc-library/__isnanl/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isnanl/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__isnormalf/main.c b/regression/cbmc-library/__isnormalf/main.c
deleted file mode 100644
index d21572bc163..00000000000
--- a/regression/cbmc-library/__isnormalf/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __isnormalf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__isnormalf/test.desc b/regression/cbmc-library/__isnormalf/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isnormalf/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__signbit/main.c b/regression/cbmc-library/__signbit/main.c
deleted file mode 100644
index e1147fa1a82..00000000000
--- a/regression/cbmc-library/__signbit/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __signbit();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__signbit/test.desc b/regression/cbmc-library/__signbit/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__signbit/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__signbitf/main.c b/regression/cbmc-library/__signbitf/main.c
deleted file mode 100644
index a34833282f3..00000000000
--- a/regression/cbmc-library/__signbitf/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __signbitf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__signbitf/test.desc b/regression/cbmc-library/__signbitf/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__signbitf/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/isfinite/main.c b/regression/cbmc-library/isfinite/main.c
index 9a739d27435..cb7aeb77c19 100644
--- a/regression/cbmc-library/isfinite/main.c
+++ b/regression/cbmc-library/isfinite/main.c
@@ -3,7 +3,18 @@
 
 int main()
 {
-  isfinite();
-  assert(0);
+  assert(isfinite(1.0));
+  assert(isfinite(1.0f));
+  assert(isfinite(1.0l));
+  float f;
+  assert(
+    !!isfinite(f) == (fpclassify(f) != FP_NAN && fpclassify(f) != FP_INFINITE));
+  double d;
+  assert(
+    !!isfinite(d) == (fpclassify(d) != FP_NAN && fpclassify(d) != FP_INFINITE));
+  long double ld;
+  assert(
+    !!isfinite(ld) ==
+    (fpclassify(ld) != FP_NAN && fpclassify(ld) != FP_INFINITE));
   return 0;
 }
diff --git a/regression/cbmc-library/isfinite/test.desc b/regression/cbmc-library/isfinite/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/isfinite/test.desc
+++ b/regression/cbmc-library/isfinite/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/isinf/main.c b/regression/cbmc-library/isinf/main.c
index 37fe2cc5d9e..18b7bb4062c 100644
--- a/regression/cbmc-library/isinf/main.c
+++ b/regression/cbmc-library/isinf/main.c
@@ -1,4 +1,5 @@
 #include <assert.h>
+#include <float.h>
 #include <math.h>
 
 #ifdef __GNUC__
@@ -21,5 +22,20 @@ int main(void)
   f00(f);
 #endif
 
+#if !defined(__clang__) && defined(__GNUC__)
+  assert(__builtin_isinf(DBL_MAX + DBL_MAX) == 1);
+  assert(__builtin_isinf(0.0) == 0);
+  assert(__builtin_isinf(-(DBL_MAX + DBL_MAX)) == 1);
+
+  assert(__builtin_isinf_sign(DBL_MAX + DBL_MAX) == 1);
+  assert(__builtin_isinf_sign(0.0) == 0);
+  assert(__builtin_isinf_sign(-(DBL_MAX + DBL_MAX)) == -1);
+
+  _Static_assert(!__builtin_isinf(0.0), "__builtin_isinf is constant");
+
+  _Static_assert(
+    __builtin_isinf_sign(0.0) == 0, "__builtin_isinf_sign is constant");
+#endif
+
   return 0;
 }
diff --git a/regression/cbmc-library/isinff/main.c b/regression/cbmc-library/isinff/main.c
deleted file mode 100644
index 083703644b2..00000000000
--- a/regression/cbmc-library/isinff/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  isinff();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/isinff/test.desc b/regression/cbmc-library/isinff/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/isinff/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/isinfl/main.c b/regression/cbmc-library/isinfl/main.c
deleted file mode 100644
index f8fcfd36425..00000000000
--- a/regression/cbmc-library/isinfl/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  isinfl();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/isinfl/test.desc b/regression/cbmc-library/isinfl/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/isinfl/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/isnanf/main.c b/regression/cbmc-library/isnanf/main.c
deleted file mode 100644
index 34b8ebb4296..00000000000
--- a/regression/cbmc-library/isnanf/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  isnanf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/isnanf/test.desc b/regression/cbmc-library/isnanf/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/isnanf/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/isnanl/main.c b/regression/cbmc-library/isnanl/main.c
deleted file mode 100644
index ef90ee15aa9..00000000000
--- a/regression/cbmc-library/isnanl/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  isnanl();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/isnanl/test.desc b/regression/cbmc-library/isnanl/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/isnanl/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/isnormal/main.c b/regression/cbmc-library/isnormal/main.c
index d4a976517e3..927306ed586 100644
--- a/regression/cbmc-library/isnormal/main.c
+++ b/regression/cbmc-library/isnormal/main.c
@@ -1,9 +1,12 @@
 #include <assert.h>
+#include <float.h>
 #include <math.h>
 
 int main()
 {
-  isnormal();
-  assert(0);
+#if !defined(__clang__) && defined(__GNUC__)
+  _Static_assert(__builtin_isnormal(DBL_MIN), "__builtin_isnormal is constant");
+#endif
+
   return 0;
 }
diff --git a/regression/cbmc-library/isnormal/test.desc b/regression/cbmc-library/isnormal/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/isnormal/test.desc
+++ b/regression/cbmc-library/isnormal/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/signbit/main.c b/regression/cbmc-library/signbit/main.c
index 111356bcd36..6e0858bf1f3 100644
--- a/regression/cbmc-library/signbit/main.c
+++ b/regression/cbmc-library/signbit/main.c
@@ -3,6 +3,13 @@
 
 int main(int argc, char **argv)
 {
+  assert(signbit(-1.0) != 0);
+  assert(signbit(1.0) == 0);
+#if !defined(__APPLE__) || __ENVIRONMENT_OS_VERSION_MIN_REQUIRED__ >= 150000
+  assert(signbit(-1.0l) != 0);
+#endif
+  assert(signbit(1.0l) == 0);
+
   float f = -0x1p-129f;
   float g = 0x1p-129f;
   float target = 0x0;
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index afc0f3ca884..35ab50c548d 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -3227,10 +3227,11 @@ exprt c_typecheck_baset::do_special_functions(
             arguments[4],
             arguments[3])))); // subnormal
   }
-  else if(identifier==CPROVER_PREFIX "isnanf" ||
-          identifier==CPROVER_PREFIX "isnand" ||
-          identifier==CPROVER_PREFIX "isnanld" ||
-          identifier=="__builtin_isnan")
+  else if(
+    identifier == CPROVER_PREFIX "isnanf" ||
+    identifier == CPROVER_PREFIX "isnand" ||
+    identifier == CPROVER_PREFIX "isnanld" || identifier == "__builtin_isnan" ||
+    identifier == "__builtin_isnanf" || identifier == "__builtin_isnanl")
   {
     if(expr.arguments().size()!=1)
     {
@@ -3246,9 +3247,12 @@ exprt c_typecheck_baset::do_special_functions(
 
     return typecast_exprt::conditional_cast(isnan_expr, expr.type());
   }
-  else if(identifier==CPROVER_PREFIX "isfinitef" ||
-          identifier==CPROVER_PREFIX "isfinited" ||
-          identifier==CPROVER_PREFIX "isfiniteld")
+  else if(
+    identifier == CPROVER_PREFIX "isfinitef" ||
+    identifier == CPROVER_PREFIX "isfinited" ||
+    identifier == CPROVER_PREFIX "isfiniteld" ||
+    identifier == "__builtin_isfinite" || identifier == "__builtin_finite" ||
+    identifier == "__builtin_finitef" || identifier == "__builtin_finitel")
   {
     if(expr.arguments().size()!=1)
     {
@@ -3321,7 +3325,8 @@ exprt c_typecheck_baset::do_special_functions(
     identifier == CPROVER_PREFIX "imaxabs" ||
     identifier == CPROVER_PREFIX "fabs" ||
     identifier == CPROVER_PREFIX "fabsf" ||
-    identifier == CPROVER_PREFIX "fabsl")
+    identifier == CPROVER_PREFIX "fabsl" || identifier == "__builtin_fabs" ||
+    identifier == "__builtin_fabsf" || identifier == "__builtin_fabsl")
   {
     if(expr.arguments().size()!=1)
     {
@@ -3453,10 +3458,11 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(old_expr);
   }
-  else if(identifier==CPROVER_PREFIX "isinff" ||
-          identifier==CPROVER_PREFIX "isinfd" ||
-          identifier==CPROVER_PREFIX "isinfld" ||
-          identifier=="__builtin_isinf")
+  else if(
+    identifier == CPROVER_PREFIX "isinff" ||
+    identifier == CPROVER_PREFIX "isinfd" ||
+    identifier == CPROVER_PREFIX "isinfld" || identifier == "__builtin_isinf" ||
+    identifier == "__builtin_isinff" || identifier == "__builtin_isinfl")
   {
     if(expr.arguments().size()!=1)
     {
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index 32b6afa9fa1..2a86bee0915 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -19,27 +19,6 @@ float fabsf(float f)
   return __CPROVER_fabsf(f);
 }
 
-/* FUNCTION: __builtin_fabs */
-
-double __builtin_fabs(double d)
-{
-  return __CPROVER_fabs(d);
-}
-
-/* FUNCTION: __builtin_fabsl */
-
-long double __builtin_fabsl(long double d)
-{
-  return __CPROVER_fabsl(d);
-}
-
-/* FUNCTION: __builtin_fabsf */
-
-float __builtin_fabsf(float f)
-{
-  return __CPROVER_fabsf(f);
-}
-
 /* FUNCTION: __CPROVER_isgreaterf */
 
 int __CPROVER_isgreaterf(float f, float g) { return f > g; }
@@ -112,6 +91,27 @@ int __finitef(float f) { return __CPROVER_isfinitef(f); }
 
 int __finitel(long double ld) { return __CPROVER_isfiniteld(ld); }
 
+/* FUNCTION: __isfinitef */
+
+int __isfinitef(float f)
+{
+  return __CPROVER_isfinitef(f);
+}
+
+/* FUNCTION: __isfinite */
+
+int __isfinite(double d)
+{
+  return __CPROVER_isfinited(d);
+}
+
+/* FUNCTION: __isfinitel */
+
+int __isfinitel(long double ld)
+{
+  return __CPROVER_isfiniteld(ld);
+}
+
 /* FUNCTION: isinf */
 
 #undef isinf
@@ -172,6 +172,13 @@ int __isnan(double d)
   return __CPROVER_isnand(d);
 }
 
+/* FUNCTION: __isnand */
+
+int __isnand(double d)
+{
+  return __CPROVER_isnand(d);
+}
+
 /* FUNCTION: __isnanf */
 
 int __isnanf(float f)
@@ -216,6 +223,20 @@ int __isnormalf(float f)
   return __CPROVER_isnormalf(f);
 }
 
+/* FUNCTION: __isnormal */
+
+int __isnormal(double d)
+{
+  return __CPROVER_isnormald(d);
+}
+
+/* FUNCTION: __isnormall */
+
+int __isnormall(long double ld)
+{
+  return __CPROVER_isnormalld(ld);
+}
+
 /* FUNCTION: __builtin_isinf */
 
 int __builtin_isinf(double d)
@@ -330,7 +351,14 @@ int __signbitf(float f)
 
 /* FUNCTION: __signbit */
 
-int __signbit(double ld)
+int __signbit(double d)
+{
+  return __CPROVER_signd(d);
+}
+
+/* FUNCTION: __signbitl */
+
+int __signbitl(long double ld)
 {
   return __CPROVER_signld(ld);
 }
@@ -3044,8 +3072,6 @@ long double log10l(long double x)
 
 int32_t __VERIFIER_nondet_int32_t(void);
 
-double __builtin_inf(void);
-
 double pow(double x, double y)
 {
   // see man pow (https://linux.die.net/man/3/pow)
@@ -3078,7 +3104,7 @@ double pow(double x, double y)
     else if(__CPROVER_signd(y))
     {
       if(fabs(x) < 1.0)
-        return __builtin_inf();
+        return __CPROVER_inf();
       else
         return +0.0;
     }
@@ -3087,7 +3113,7 @@ double pow(double x, double y)
       if(fabs(x) < 1.0)
         return +0.0;
       else
-        return __builtin_inf();
+        return __CPROVER_inf();
     }
   }
   else if(isinf(x) && __CPROVER_signd(x))
@@ -3102,9 +3128,9 @@ double pow(double x, double y)
     else
     {
       if(nearbyint(y) == y && fabs(fmod(y, 2.0)) == 1.0)
-        return -__builtin_inf();
+        return -__CPROVER_inf();
       else
-        return __builtin_inf();
+        return __CPROVER_inf();
     }
   }
   else if(isinf(x) && !__CPROVER_signd(x))
@@ -3112,7 +3138,7 @@ double pow(double x, double y)
     if(__CPROVER_signd(y))
       return +0.0;
     else
-      return __builtin_inf();
+      return __CPROVER_inf();
   }
   else if(fpclassify(x) == FP_ZERO && __CPROVER_signd(y))
   {
@@ -3192,8 +3218,6 @@ double pow(double x, double y)
 
 int32_t __VERIFIER_nondet_int32_t(void);
 
-float __builtin_inff(void);
-
 float powf(float x, float y)
 {
   // see man pow (https://linux.die.net/man/3/pow)
@@ -3226,7 +3250,7 @@ float powf(float x, float y)
     else if(__CPROVER_signf(y))
     {
       if(fabsf(x) < 1.0f)
-        return __builtin_inff();
+        return __CPROVER_inff();
       else
         return +0.0f;
     }
@@ -3235,7 +3259,7 @@ float powf(float x, float y)
       if(fabsf(x) < 1.0f)
         return +0.0f;
       else
-        return __builtin_inff();
+        return __CPROVER_inff();
     }
   }
   else if(isinff(x) && __CPROVER_signf(x))
@@ -3250,9 +3274,9 @@ float powf(float x, float y)
     else
     {
       if(nearbyintf(y) == y && fabsf(fmodf(y, 2.0f)) == 1.0f)
-        return -__builtin_inff();
+        return -__CPROVER_inff();
       else
-        return __builtin_inff();
+        return __CPROVER_inff();
     }
   }
   else if(isinff(x) && !__CPROVER_signf(x))
@@ -3260,7 +3284,7 @@ float powf(float x, float y)
     if(__CPROVER_signf(y))
       return +0.0f;
     else
-      return __builtin_inff();
+      return __CPROVER_inff();
   }
   else if(fpclassify(x) == FP_ZERO && __CPROVER_signf(y))
   {
@@ -3337,8 +3361,6 @@ float powf(float x, float y)
 
 int32_t __VERIFIER_nondet_int32_t(void);
 
-long double __builtin_infl(void);
-
 long double powl(long double x, long double y)
 {
   // see man pow (https://linux.die.net/man/3/pow)
@@ -3371,7 +3393,7 @@ long double powl(long double x, long double y)
     else if(__CPROVER_signld(y))
     {
       if(fabsl(x) < 1.0l)
-        return __builtin_infl();
+        return __CPROVER_infl();
       else
         return +0.0l;
     }
@@ -3380,7 +3402,7 @@ long double powl(long double x, long double y)
       if(fabsl(x) < 1.0l)
         return +0.0l;
       else
-        return __builtin_infl();
+        return __CPROVER_infl();
     }
   }
   else if(isinfl(x) && __CPROVER_signld(x))
@@ -3395,9 +3417,9 @@ long double powl(long double x, long double y)
     else
     {
       if(nearbyintl(y) == y && fabsl(fmodl(y, 2.0l)) == 1.0l)
-        return -__builtin_infl();
+        return -__CPROVER_infl();
       else
-        return __builtin_infl();
+        return __CPROVER_infl();
     }
   }
   else if(isinfl(x) && !__CPROVER_signld(x))
@@ -3405,7 +3427,7 @@ long double powl(long double x, long double y)
     if(__CPROVER_signld(y))
       return +0.0f;
     else
-      return __builtin_infl();
+      return __CPROVER_infl();
   }
   else if(fpclassify(x) == FP_ZERO && __CPROVER_signld(y))
   {
@@ -3578,8 +3600,6 @@ long double fmal(long double x, long double y, long double z)
 
 int32_t __VERIFIER_nondet_int32_t(void);
 
-double __builtin_inf(void);
-
 double __builtin_powi(double x, int y)
 {
   // see man pow (https://linux.die.net/man/3/pow), specialized for y being an
@@ -3607,9 +3627,9 @@ double __builtin_powi(double x, int y)
     else
     {
       if(y % 2 == 1)
-        return -__builtin_inf();
+        return -__CPROVER_inf();
       else
-        return __builtin_inf();
+        return __CPROVER_inf();
     }
   }
   else if(isinf(x) && !__CPROVER_signd(x))
@@ -3617,7 +3637,7 @@ double __builtin_powi(double x, int y)
     if(y < 0)
       return +0.0;
     else
-      return __builtin_inf();
+      return __CPROVER_inf();
   }
   else if(fpclassify(x) == FP_ZERO && y < 0)
   {
@@ -3697,8 +3717,6 @@ double __builtin_powi(double x, int y)
 
 int32_t __VERIFIER_nondet_int32_t(void);
 
-float __builtin_inff(void);
-
 float __builtin_powif(float x, int y)
 {
   // see man pow (https://linux.die.net/man/3/pow), specialized for y being an
@@ -3726,9 +3744,9 @@ float __builtin_powif(float x, int y)
     else
     {
       if(y % 2 == 1)
-        return -__builtin_inff();
+        return -__CPROVER_inff();
       else
-        return __builtin_inff();
+        return __CPROVER_inff();
     }
   }
   else if(isinff(x) && !__CPROVER_signf(x))
@@ -3736,7 +3754,7 @@ float __builtin_powif(float x, int y)
     if(y < 0)
       return +0.0f;
     else
-      return __builtin_inff();
+      return __CPROVER_inff();
   }
   else if(fpclassify(x) == FP_ZERO && y < 0)
   {
@@ -3812,7 +3830,6 @@ float __builtin_powif(float x, int y)
 
 int32_t __VERIFIER_nondet_int32_t(void);
 
-long double __builtin_infl(void);
 double __builtin_powi(double, int);
 
 long double __builtin_powil(long double x, int y)
@@ -3842,9 +3859,9 @@ long double __builtin_powil(long double x, int y)
     else
     {
       if(y % 2 == 1)
-        return -__builtin_infl();
+        return -__CPROVER_infl();
       else
-        return __builtin_infl();
+        return __CPROVER_infl();
     }
   }
   else if(isinf(x) && !__CPROVER_signld(x))
@@ -3852,7 +3869,7 @@ long double __builtin_powil(long double x, int y)
     if(y < 0)
       return +0.0f;
     else
-      return __builtin_infl();
+      return __CPROVER_infl();
   }
   else if(fpclassify(x) == FP_ZERO && y < 0)
   {
diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh
index 6883984ae26..5902b79aba1 100755
--- a/src/ansi-c/library_check.sh
+++ b/src/ansi-c/library_check.sh
@@ -68,12 +68,19 @@ perl -p -i -e 's/^__builtin_alloca\n//' __functions # alloca-01
 perl -p -i -e 's/^fclose_cleanup\n//' __functions # fopen
 perl -p -i -e 's/^fopen64\n//' __functions # fopen
 perl -p -i -e 's/^freopen64\n//' __functions # freopen
+perl -p -i -e 's/^isinf[fl]\n//' __functions # isinf
+perl -p -i -e 's/^isnan[fl]\n//' __functions # isnan
 perl -p -i -e 's/^mmap64\n//' __functions # mmap
 perl -p -i -e 's/^munmap\n//' __functions # mmap-01
 perl -p -i -e 's/^__fgets_chk\n//' __functions # fgets/__fgets_chk.desc
 perl -p -i -e 's/^__fprintf_chk\n//' __functions # fprintf/__fprintf_chk.desc
 perl -p -i -e 's/^__fread_chk\n//' __functions # fread/__fread_chk.desc
+perl -p -i -e 's/^__isfinite[fl]?\n//' __functions # isfinite
+perl -p -i -e 's/^__isinf[fl]?\n//' __functions # isinf
+perl -p -i -e 's/^__isnan[dfl]?\n//' __functions # isnan
+perl -p -i -e 's/^__isnormal[fl]?\n//' __functions # isnormal
 perl -p -i -e 's/^__printf_chk\n//' __functions # printf/__printf_chk.desc
+perl -p -i -e 's/^__signbit[fl]?\n//' __functions # signbit, __signbitd
 perl -p -i -e 's/^__syslog_chk\n//' __functions # syslog/__syslog_chk.desc
 perl -p -i -e 's/^_syslog\$DARWIN_EXTSN\n//' __functions # syslog/test.desc
 perl -p -i -e 's/^__time64\n//' __functions # time

From 73ed258fce0d00326a7cf3db69a81248907c46a2 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 29 May 2026 17:11:07 +0000
Subject: [PATCH 2/2] Fix --nan-check false positives in division and
 multiplication branches

Two fixes in goto_check_ct::nan_check:

1. Division: the existing condition treated x/inf as a NaN-producing
   operation, but per IEEE 754-2019 Section 6.1, finite/inf is +/-0,
   not NaN. The only div operations that produce NaN are 0/0 and
   inf/inf. Replace the over-broad isinf(op1) check with the
   conjunction isinf(op0) && isinf(op1).

2. Multiplication: the zero_times_inf clause was a copy-paste of
   inf_times_zero (both compared op1 against zero and op0 against
   isinf), so --nan-check failed to flag '0 * inf' when the zero
   was on the LHS. Fix by swapping the operand sides in
   zero_times_inf.

The companion ieee_float.cpp comment update brings the runtime
constant evaluator's comment in line with the now-correct semantics
(it already evaluated both directions correctly; only the comment
was misleading).

New regression tests:
- regression/cbmc/float-finite-div-infinity: positive test that
  finite/inf produces +/-0.0 with --nan-check enabled, no NaN
  assertion fired.
- regression/cbmc/float-inf-div-inf: positive test that inf/inf is
  flagged as NaN under all four sign permutations.
- regression/cbmc/float-nan-check: replace the (now-incorrect) n/inf
  case with inf/inf, and add a 'myzero * myinf' assertion that the
  buggy mult-branch was missing -- without fix 2, that assertion is
  not generated and the test fails.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 .../cbmc/float-finite-div-infinity/main.c     | 49 +++++++++++++++++++
 .../cbmc/float-finite-div-infinity/test.desc  | 12 +++++
 regression/cbmc/float-inf-div-inf/main.c      | 28 +++++++++++
 regression/cbmc/float-inf-div-inf/test.desc   | 15 ++++++
 regression/cbmc/float-nan-check/main.c        |  7 ++-
 regression/cbmc/float-nan-check/test.desc     | 33 +++++++------
 src/ansi-c/goto-conversion/goto_check_c.cpp   | 40 ++++++++-------
 src/util/ieee_float.cpp                       |  2 +-
 8 files changed, 148 insertions(+), 38 deletions(-)
 create mode 100644 regression/cbmc/float-finite-div-infinity/main.c
 create mode 100644 regression/cbmc/float-finite-div-infinity/test.desc
 create mode 100644 regression/cbmc/float-inf-div-inf/main.c
 create mode 100644 regression/cbmc/float-inf-div-inf/test.desc

diff --git a/regression/cbmc/float-finite-div-infinity/main.c b/regression/cbmc/float-finite-div-infinity/main.c
new file mode 100644
index 00000000000..eca8189a4d0
--- /dev/null
+++ b/regression/cbmc/float-finite-div-infinity/main.c
@@ -0,0 +1,49 @@
+// Test case for bug fix: finite / +INFINITY should NOT trigger --nan-check
+// According to IEEE 754-2019 Section 6.1: "division(x, ∞) for finite x"
+// should produce 0.0, not NaN. Hence, none of the operations below should
+// trigger nan-check assertions.
+
+#include <assert.h>
+#include <math.h>
+#include <stdint.h>
+
+union float_bits
+{
+  uint32_t u;
+  float f;
+};
+
+int main(void)
+{
+  // Test case 1: Using union to create +INFINITY as mentioned in the bug report
+  union float_bits a, b;
+  a.u = 1065353216; // 1.0
+  b.u = 2139095040; // +INF
+
+  // This should produce 0.0, not NaN - should NOT trigger nan-check failure
+  float result1 = a.f / b.f;
+  assert(fpclassify(result1) == FP_ZERO && !signbit(result1));
+
+  // Test case 2: Direct assignment as mentioned in the bug report
+  float x = 1.0f;
+  float y = INFINITY;
+  float result2 = x / y;
+  assert(fpclassify(result2) == FP_ZERO && !signbit(result2));
+
+  // Test case 3: Negative finite / infinity should also be 0.0 (negative zero)
+  float neg_x = -1.0f;
+  float result3 = neg_x / INFINITY;
+  assert(fpclassify(result3) == FP_ZERO && signbit(result3));
+
+  // Test case 4: Various finite values divided by infinity
+  float nd_positive = __VERIFIER_nondet_float();
+  __CPROVER_assume(isfinite(nd_positive) && nd_positive > 0);
+  float result4 = nd_positive / INFINITY;
+  assert(fpclassify(result4) == FP_ZERO && !signbit(result4));
+  float nd_negative = __VERIFIER_nondet_float();
+  __CPROVER_assume(isfinite(nd_negative) && nd_negative < 0);
+  float result5 = nd_negative / INFINITY;
+  assert(fpclassify(result5) == FP_ZERO && signbit(result5));
+
+  return 0;
+}
diff --git a/regression/cbmc/float-finite-div-infinity/test.desc b/regression/cbmc/float-finite-div-infinity/test.desc
new file mode 100644
index 00000000000..5b46e27c588
--- /dev/null
+++ b/regression/cbmc/float-finite-div-infinity/test.desc
@@ -0,0 +1,12 @@
+CORE no-new-smt broken-cprover-smt-backend
+main.c
+--nan-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test verifies that dividing a finite float by +INFINITY does NOT
+incorrectly trigger a NaN check failure (bug fix). According to IEEE 754-2019
+Section 6.1, division(x, ∞) for finite x = 0.0. Only inf/inf should produce NaN
+(which is covered in test float-inf-div-inf)
diff --git a/regression/cbmc/float-inf-div-inf/main.c b/regression/cbmc/float-inf-div-inf/main.c
new file mode 100644
index 00000000000..c3738656e2b
--- /dev/null
+++ b/regression/cbmc/float-inf-div-inf/main.c
@@ -0,0 +1,28 @@
+// Test case for bug fix: inf / inf SHOULD trigger --nan-check failure
+// According to IEEE 754-2019, inf/inf produces NaN
+
+#include <assert.h>
+#include <math.h>
+
+int main(void)
+{
+  // Ensure infinity / infinity produces NaN and triggers nan-check
+  float inf1 = INFINITY;
+  float inf2 = INFINITY;
+  float result1 = inf1 / inf2; // Should trigger NaN check
+  assert(isnan(result1));
+
+  // Also test -inf / inf
+  float result2 = (-INFINITY) / INFINITY; // Should trigger NaN check
+  assert(isnan(result2));
+
+  // And inf / -inf
+  float result3 = INFINITY / (-INFINITY); // Should trigger NaN check
+  assert(isnan(result3));
+
+  // And -inf / -inf
+  float result4 = (-INFINITY) / (-INFINITY); // Should trigger NaN check
+  assert(isnan(result4));
+
+  return 0;
+}
diff --git a/regression/cbmc/float-inf-div-inf/test.desc b/regression/cbmc/float-inf-div-inf/test.desc
new file mode 100644
index 00000000000..e7fffb4ca33
--- /dev/null
+++ b/regression/cbmc/float-inf-div-inf/test.desc
@@ -0,0 +1,15 @@
+CORE
+main.c
+--nan-check
+\[main.NaN.1\] line \d+ NaN on / in inf1 / inf2: FAILURE
+\[main.NaN.2\] line \d+ NaN on / in -(\+INFINITY|return_value___builtin_(huge_val|inf)f\$\d+|\(\(float\)1\.000000e\+300\)) / (\+INFINITY|return_value___builtin_(huge_val|inf)f\$\d+|\(float\)1\.000000e\+300): FAILURE
+\[main.NaN.3\] line \d+ NaN on / in (\+INFINITY|return_value___builtin_(huge_val|inf)f\$\d+|\(float\)1\.000000e\+300) / -(\+INFINITY|return_value___builtin_(huge_val|inf)f\$\d+|\(\(float\)1\.000000e\+300\)): FAILURE
+\[main.NaN.4\] line \d+ NaN on / in -(\+INFINITY|return_value___builtin_(huge_val|inf)f\$\d+|\(\(float\)1\.000000e\+300\)) / -(\+INFINITY|return_value___builtin_(huge_val|inf)f\$\d+|\(\(float\)1\.000000e\+300\)): FAILURE
+^\*\* 4 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test verifies that inf/inf correctly triggers NaN check failures.
+According to IEEE 754-2019, inf/inf = NaN.
diff --git a/regression/cbmc/float-nan-check/main.c b/regression/cbmc/float-nan-check/main.c
index 66d39556905..9467765fec9 100644
--- a/regression/cbmc/float-nan-check/main.c
+++ b/regression/cbmc/float-nan-check/main.c
@@ -39,10 +39,13 @@ int main(void)
   // these operations should generate assertions
   // 0.0 / 0.0 = NaN
   f = myzero / myzero;
-  // n / Inf = NaN
-  f = n / (myinf);
+  // Inf / Inf = NaN (per IEEE 754-2019 Section 6.1)
+  f = myinf / myinf;
   // Inf * 0 = NaN
   f = (myinf)*myzero;
+  // 0 * Inf = NaN (this direction caught by the goto_check_c.cpp
+  // mult-branch fix accompanying this commit)
+  f = myzero * (myinf);
   // -Inf + Inf = NaN
   f = (-myinf) + (myinf);
   // Inf + (-Inf) = NaN
diff --git a/regression/cbmc/float-nan-check/test.desc b/regression/cbmc/float-nan-check/test.desc
index 92033bd0a16..fad08d3ab8c 100644
--- a/regression/cbmc/float-nan-check/test.desc
+++ b/regression/cbmc/float-nan-check/test.desc
@@ -3,24 +3,25 @@ main.c
 --nan-check
 \[main.NaN.1\] line \d+ NaN on \+ in byte_extract_(big|little)_endian\(c, (0|0l|0ll), float\) \+ myzero: SUCCESS
 \[main.NaN.2\] line \d+ NaN on / in myzero / myzero: FAILURE
-\[main.NaN.3\] line \d+ NaN on / in \(float\)n / myinf: FAILURE
+\[main.NaN.3\] line \d+ NaN on / in myinf / myinf: FAILURE
 \[main.NaN.4\] line \d+ NaN on \* in myinf \* myzero: FAILURE
-\[main.NaN.5\] line \d+ NaN on \+ in -myinf \+ myinf: FAILURE
-\[main.NaN.6\] line \d+ NaN on \+ in myinf \+ -myinf: FAILURE
-\[main.NaN.7\] line \d+ NaN on - in myinf - myinf: FAILURE
-\[main.NaN.8\] line \d+ NaN on - in -myinf - -myinf: FAILURE
-\[main.NaN.9\] line \d+ NaN on \+ in byte_extract_(big|little)_endian\(c, (0|0l|0ll), float\) \+ byte_extract_(big|little)_endian\(c, (0|0l|0ll), float\): SUCCESS
-\[main.NaN.10\] line \d+ NaN on / in byte_extract_(big|little)_endian\(c, (0|0l|0ll), float\) / myzero: SUCCESS
-\[main.NaN.11\] line \d+ NaN on \* in mynan \* mynan: SUCCESS
-\[main.NaN.12\] line \d+ NaN on \+ in mynan \+ mynan: SUCCESS
-\[main.NaN.13\] line \d+ NaN on - in mynan - mynan: SUCCESS
-\[main.NaN.14\] line \d+ NaN on / in mynan / mynan: SUCCESS
-\[main.NaN.15\] line \d+ NaN on \+ in mynan \+ \(float\)n: SUCCESS
-\[main.NaN.16\] line \d+ NaN on - in mynan - \(float\)n: SUCCESS
-\[main.NaN.17\] line \d+ NaN on \* in mynan \* \(float\)n: SUCCESS
-\[main.NaN.18\] line \d+ NaN on / in mynan / \(float\)n: SUCCESS
+\[main.NaN.5\] line \d+ NaN on \* in myzero \* myinf: FAILURE
+\[main.NaN.6\] line \d+ NaN on \+ in -myinf \+ myinf: FAILURE
+\[main.NaN.7\] line \d+ NaN on \+ in myinf \+ -myinf: FAILURE
+\[main.NaN.8\] line \d+ NaN on - in myinf - myinf: FAILURE
+\[main.NaN.9\] line \d+ NaN on - in -myinf - -myinf: FAILURE
+\[main.NaN.10\] line \d+ NaN on \+ in byte_extract_(big|little)_endian\(c, (0|0l|0ll), float\) \+ byte_extract_(big|little)_endian\(c, (0|0l|0ll), float\): SUCCESS
+\[main.NaN.11\] line \d+ NaN on / in byte_extract_(big|little)_endian\(c, (0|0l|0ll), float\) / myzero: SUCCESS
+\[main.NaN.12\] line \d+ NaN on \* in mynan \* mynan: SUCCESS
+\[main.NaN.13\] line \d+ NaN on \+ in mynan \+ mynan: SUCCESS
+\[main.NaN.14\] line \d+ NaN on - in mynan - mynan: SUCCESS
+\[main.NaN.15\] line \d+ NaN on / in mynan / mynan: SUCCESS
+\[main.NaN.16\] line \d+ NaN on \+ in mynan \+ \(float\)n: SUCCESS
+\[main.NaN.17\] line \d+ NaN on - in mynan - \(float\)n: SUCCESS
+\[main.NaN.18\] line \d+ NaN on \* in mynan \* \(float\)n: SUCCESS
+\[main.NaN.19\] line \d+ NaN on / in mynan / \(float\)n: SUCCESS
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
-\[main.NaN.19\]
+\[main.NaN.20\]
diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp
index ad0419853a9..89d0317b538 100644
--- a/src/ansi-c/goto-conversion/goto_check_c.cpp
+++ b/src/ansi-c/goto-conversion/goto_check_c.cpp
@@ -1253,18 +1253,20 @@ void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
   {
     const auto &div_expr = to_div_expr(expr);
 
-    // there a two ways to get a new NaN on division:
-    // 0/0 = NaN and x/inf = NaN
+    // there are two ways to get a new NaN on division:
+    // 0/0 = NaN and inf/inf = NaN
     // (note that x/0 = +-inf for x!=0 and x!=inf)
-    const and_exprt zero_div_zero(
-      ieee_float_equal_exprt(
-        div_expr.op0(), from_integer(0, div_expr.dividend().type())),
-      ieee_float_equal_exprt(
-        div_expr.op1(), from_integer(0, div_expr.divisor().type())));
+    // (note that finite/inf = +-0.0, NOT NaN per IEEE 754-2019 Section 6.1)
+    and_exprt zero_div_zero{
+      ieee_float_equal_exprt{
+        div_expr.op0(), from_integer(0, div_expr.dividend().type())},
+      ieee_float_equal_exprt{
+        div_expr.op1(), from_integer(0, div_expr.divisor().type())}};
 
-    const isinf_exprt div_inf(div_expr.op1());
+    and_exprt inf_div_inf{
+      isinf_exprt{div_expr.op0()}, isinf_exprt{div_expr.op1()}};
 
-    isnan = or_exprt(zero_div_zero, div_inf);
+    isnan = or_exprt{std::move(zero_div_zero), std::move(inf_div_inf)};
   }
   else if(expr.id() == ID_mult)
   {
@@ -1273,18 +1275,18 @@ void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
 
     const auto &mult_expr = to_mult_expr(expr);
 
-    // Inf * 0 is NaN
-    const and_exprt inf_times_zero(
-      isinf_exprt(mult_expr.op0()),
-      ieee_float_equal_exprt(
-        mult_expr.op1(), from_integer(0, mult_expr.op1().type())));
+    // Inf * 0 is NaN, in either operand order.
+    and_exprt inf_times_zero{
+      isinf_exprt{mult_expr.op0()},
+      ieee_float_equal_exprt{
+        mult_expr.op1(), from_integer(0, mult_expr.op1().type())}};
 
-    const and_exprt zero_times_inf(
-      ieee_float_equal_exprt(
-        mult_expr.op1(), from_integer(0, mult_expr.op1().type())),
-      isinf_exprt(mult_expr.op0()));
+    and_exprt zero_times_inf{
+      ieee_float_equal_exprt{
+        mult_expr.op0(), from_integer(0, mult_expr.op0().type())},
+      isinf_exprt{mult_expr.op1()}};
 
-    isnan = or_exprt(inf_times_zero, zero_times_inf);
+    isnan = or_exprt{std::move(inf_times_zero), std::move(zero_times_inf)};
   }
   else if(expr.id() == ID_plus)
   {
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
index 497a9558471..f966d9333dc 100644
--- a/src/util/ieee_float.cpp
+++ b/src/util/ieee_float.cpp
@@ -1051,7 +1051,7 @@ ieee_floatt &ieee_floatt::operator/=(const ieee_floatt &other)
     return *this;
   }
 
-  // x/inf = NaN
+  // inf/inf = NaN, x/inf = 0 for finite x
   if(other.infinity_flag)
   {
     if(infinity_flag)