diff --git a/regression/cbmc-library/__builtin_inf-01/main.c b/regression/cbmc-library/__builtin_inf-01/main.c
deleted file mode 100644
index 167b7806f23..00000000000
--- a/regression/cbmc-library/__builtin_inf-01/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_inf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_inff-01/main.c b/regression/cbmc-library/__builtin_inff-01/main.c
deleted file mode 100644
index a043bdf030a..00000000000
--- a/regression/cbmc-library/__builtin_inff-01/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_inff();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_inff-01/test.desc b/regression/cbmc-library/__builtin_inff-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_inff-01/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_infl-01/main.c b/regression/cbmc-library/__builtin_infl-01/main.c
deleted file mode 100644
index 411b2bc1bd6..00000000000
--- a/regression/cbmc-library/__builtin_infl-01/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_infl();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_infl-01/test.desc b/regression/cbmc-library/__builtin_infl-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_infl-01/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/builtin_inf/static_init.c b/regression/cbmc/builtin_inf/static_init.c
new file mode 100644
index 00000000000..d286fb5013a
--- /dev/null
+++ b/regression/cbmc/builtin_inf/static_init.c
@@ -0,0 +1,42 @@
+#include <assert.h>
+#include <math.h>
+
+float g = -INFINITY;
+
+void test_static_float_infinity()
+{
+  static float f = +INFINITY;
+  assert(isinf(f));
+}
+
+void test_static_double_infinity()
+{
+  static double d = INFINITY;
+  assert(isinf(d));
+}
+
+void test_static_long_double_infinity()
+{
+  static long double ld = INFINITY;
+  assert(isinf(ld));
+}
+
+void test_static_huge_val()
+{
+  static float f = HUGE_VALF;
+  static double d = HUGE_VAL;
+  static long double ld = HUGE_VALL;
+
+  assert(isinf(f));
+  assert(isinf(d));
+  assert(isinf(ld));
+}
+
+int main()
+{
+  test_static_float_infinity();
+  test_static_double_infinity();
+  test_static_long_double_infinity();
+  test_static_huge_val();
+  return 0;
+}
diff --git a/regression/cbmc-library/__builtin_inf-01/test.desc b/regression/cbmc/builtin_inf/test.desc
similarity index 59%
rename from regression/cbmc-library/__builtin_inf-01/test.desc
rename to regression/cbmc/builtin_inf/test.desc
index 9542d988e8d..c5a79d4cd67 100644
--- a/regression/cbmc-library/__builtin_inf-01/test.desc
+++ b/regression/cbmc/builtin_inf/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
+CORE
+static_init.c
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index b5799f315f3..d2219a7a29a 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -3265,8 +3265,9 @@ exprt c_typecheck_baset::do_special_functions(
 
     return typecast_exprt::conditional_cast(isfinite_expr, expr.type());
   }
-  else if(identifier==CPROVER_PREFIX "inf" ||
-          identifier=="__builtin_inf")
+  else if(
+    identifier == CPROVER_PREFIX "inf" || identifier == "__builtin_inf" ||
+    identifier == "__builtin_huge_val")
   {
     constant_exprt inf_expr=
       ieee_floatt::plus_infinity(
@@ -3275,7 +3276,9 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(inf_expr);
   }
-  else if(identifier==CPROVER_PREFIX "inff")
+  else if(
+    identifier == CPROVER_PREFIX "inff" || identifier == "__builtin_inff" ||
+    identifier == "__builtin_huge_valf")
   {
     constant_exprt inff_expr=
       ieee_floatt::plus_infinity(
@@ -3284,7 +3287,9 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(inff_expr);
   }
-  else if(identifier==CPROVER_PREFIX "infl")
+  else if(
+    identifier == CPROVER_PREFIX "infl" || identifier == "__builtin_infl" ||
+    identifier == "__builtin_huge_vall")
   {
     floatbv_typet type=to_floatbv_type(long_double_type());
     constant_exprt infl_expr=
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index ac594c0e590..c8cf190fc8e 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -216,39 +216,6 @@ int __isnormalf(float f)
   return __CPROVER_isnormalf(f);
 }
 
-/* FUNCTION: __builtin_inff */
-
-float __builtin_inff(void)
-{
-#pragma CPROVER check push
-#pragma CPROVER check disable "float-div-by-zero"
-#pragma CPROVER check disable "float-overflow"
-  return 1.0f / 0.0f;
-#pragma CPROVER check pop
-}
-
-/* FUNCTION: __builtin_inf */
-
-double __builtin_inf(void)
-{
-#pragma CPROVER check push
-#pragma CPROVER check disable "float-div-by-zero"
-#pragma CPROVER check disable "float-overflow"
-  return 1.0 / 0.0;
-#pragma CPROVER check pop
-}
-
-/* FUNCTION: __builtin_infl */
-
-long double __builtin_infl(void)
-{
-#pragma CPROVER check push
-#pragma CPROVER check disable "float-div-by-zero"
-#pragma CPROVER check disable "float-overflow"
-  return 1.0l / 0.0l;
-#pragma CPROVER check pop
-}
-
 /* FUNCTION: __builtin_isinf */
 
 int __builtin_isinf(double d)