diff --git a/.github/workflows/bsd.yaml b/.github/workflows/bsd.yaml
index 52d738f1d8b..6674b2a7f38 100644
--- a/.github/workflows/bsd.yaml
+++ b/.github/workflows/bsd.yaml
@@ -63,6 +63,7 @@ jobs:
             # gmake TAGS='[!shouldfail]' -C jbmc/unit test
             echo "Run regression tests"
             gmake -C regression/cbmc test
+            gmake -C regression/cbmc-library test
             # gmake -C regression test-parallel JOBS=2
             # gmake -C regression/cbmc test-paths-lifo
             # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
@@ -125,6 +126,10 @@ jobs:
             # gmake TAGS='[!shouldfail]' -C jbmc/unit test
             echo "Run regression tests"
             gmake -C regression/cbmc test
+            # TODO: fileno and *fprintf tests are failing, requires debugging
+            # https://github.com/openbsd/src/blob/master/include/stdio.h may be
+            # useful (likely need to allocate __sF)
+            gmake -C regression/cbmc-library test || true
             # gmake -C regression test-parallel JOBS=2
             # gmake -C regression/cbmc test-paths-lifo
             # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
@@ -190,6 +195,7 @@ jobs:
             echo "Run regression tests"
             # TODO: we need to model some more library functions
             gmake -C regression/cbmc test || true
+            gmake -C regression/cbmc-library test || true
             # gmake -C regression test-parallel JOBS=2
             # gmake -C regression/cbmc test-paths-lifo
             # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
diff --git a/regression/cbmc-library/__builtin_fabs-01/main.c b/regression/cbmc-library/__builtin_fabs-01/main.c
deleted file mode 100644
index 38b521fe15c..00000000000
--- a/regression/cbmc-library/__builtin_fabs-01/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-01/test.desc b/regression/cbmc-library/__builtin_fabs-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_fabs-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_fabsf-01/main.c b/regression/cbmc-library/__builtin_fabsf-01/main.c
deleted file mode 100644
index 7c4cc5cc1fd..00000000000
--- a/regression/cbmc-library/__builtin_fabsf-01/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-01/test.desc b/regression/cbmc-library/__builtin_fabsf-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_fabsf-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_fabsl-01/main.c b/regression/cbmc-library/__builtin_fabsl-01/main.c
deleted file mode 100644
index 6e69656f497..00000000000
--- a/regression/cbmc-library/__builtin_fabsl-01/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-01/test.desc b/regression/cbmc-library/__builtin_fabsl-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_fabsl-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_huge_val-01/main.c b/regression/cbmc-library/__builtin_huge_val-01/main.c
deleted file mode 100644
index acebd77a7c0..00000000000
--- a/regression/cbmc-library/__builtin_huge_val-01/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_huge_val();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_huge_val-01/test.desc b/regression/cbmc-library/__builtin_huge_val-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_huge_val-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_huge_valf-01/main.c b/regression/cbmc-library/__builtin_huge_valf-01/main.c
deleted file mode 100644
index acd2d8f592b..00000000000
--- a/regression/cbmc-library/__builtin_huge_valf-01/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_huge_valf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_huge_valf-01/test.desc b/regression/cbmc-library/__builtin_huge_valf-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_huge_valf-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_huge_vall-01/main.c b/regression/cbmc-library/__builtin_huge_vall-01/main.c
deleted file mode 100644
index 7354750277b..00000000000
--- a/regression/cbmc-library/__builtin_huge_vall-01/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_huge_vall();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_huge_vall-01/test.desc b/regression/cbmc-library/__builtin_huge_vall-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_huge_vall-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_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_inf-01/test.desc b/regression/cbmc-library/__builtin_inf-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_inf-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_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-library/__builtin_isinf-01/main.c b/regression/cbmc-library/__builtin_isinf-01/main.c
deleted file mode 100644
index 7b7ba2981a2..00000000000
--- a/regression/cbmc-library/__builtin_isinf-01/main.c
+++ /dev/null
@@ -1,55 +0,0 @@
-#include <assert.h>
-#include <float.h>
-#include <math.h>
-
-int main()
-{
-  double xxx;
-
-// 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);
-
-  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);
-
-  // these are compile-time
-  _Static_assert(
-    __builtin_fpclassify(0, 1, 2, 3, 4, -0.0) == 4,
-    "__builtin_fpclassify is constant");
-
-  _Static_assert(__builtin_isnormal(DBL_MIN), "__builtin_isnormal is constant");
-
-  _Static_assert(!__builtin_isinf(0.0), "__builtin_isinf is constant");
-
-  _Static_assert(
-    __builtin_isinf_sign(0.0) == 0, "__builtin_isinf_sign is constant");
-
-#endif
-
-  assert(signbit(-1.0) != 0);
-  assert(signbit(1.0) == 0);
-}
diff --git a/regression/cbmc-library/__builtin_isinf-01/test.desc b/regression/cbmc-library/__builtin_isinf-01/test.desc
deleted file mode 100644
index b7d95a28215..00000000000
--- a/regression/cbmc-library/__builtin_isinf-01/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-CORE
-main.c
---floatbv
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__builtin_isinff-01/main.c b/regression/cbmc-library/__builtin_isinff-01/main.c
deleted file mode 100644
index a1b7043aff7..00000000000
--- a/regression/cbmc-library/__builtin_isinff-01/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_isinff();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_isinff-01/test.desc b/regression/cbmc-library/__builtin_isinff-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_isinff-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_isnan-01/main.c b/regression/cbmc-library/__builtin_isnan-01/main.c
deleted file mode 100644
index 812cb90633e..00000000000
--- a/regression/cbmc-library/__builtin_isnan-01/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_isnan();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_isnan-01/test.desc b/regression/cbmc-library/__builtin_isnan-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_isnan-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_isnanf-01/main.c b/regression/cbmc-library/__builtin_isnanf-01/main.c
deleted file mode 100644
index c34ad07ad20..00000000000
--- a/regression/cbmc-library/__builtin_isnanf-01/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_isnanf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_isnanf-01/test.desc b/regression/cbmc-library/__builtin_isnanf-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_isnanf-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/__fpclassify-01/main.c b/regression/cbmc-library/__fpclassify-01/main.c
index 8b05699e4a6..fbbeffb63a6 100644
--- a/regression/cbmc-library/__fpclassify-01/main.c
+++ b/regression/cbmc-library/__fpclassify-01/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-01/main.c b/regression/cbmc-library/__isinf-01/main.c
deleted file mode 100644
index 3441084533d..00000000000
--- a/regression/cbmc-library/__isinf-01/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-01/test.desc b/regression/cbmc-library/__isinf-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isinf-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/__isinff-01/main.c b/regression/cbmc-library/__isinff-01/main.c
deleted file mode 100644
index 446e25a9512..00000000000
--- a/regression/cbmc-library/__isinff-01/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-01/test.desc b/regression/cbmc-library/__isinff-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isinff-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/__isinfl-01/main.c b/regression/cbmc-library/__isinfl-01/main.c
deleted file mode 100644
index df21c681f43..00000000000
--- a/regression/cbmc-library/__isinfl-01/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-01/test.desc b/regression/cbmc-library/__isinfl-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isinfl-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/__isnan-01/main.c b/regression/cbmc-library/__isnan-01/main.c
deleted file mode 100644
index 3bd8ba542ca..00000000000
--- a/regression/cbmc-library/__isnan-01/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-01/test.desc b/regression/cbmc-library/__isnan-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isnan-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/__isnanf-01/main.c b/regression/cbmc-library/__isnanf-01/main.c
deleted file mode 100644
index 074fea3bf29..00000000000
--- a/regression/cbmc-library/__isnanf-01/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-01/test.desc b/regression/cbmc-library/__isnanf-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isnanf-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/__isnanl-01/main.c b/regression/cbmc-library/__isnanl-01/main.c
deleted file mode 100644
index bdda6af323e..00000000000
--- a/regression/cbmc-library/__isnanl-01/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-01/test.desc b/regression/cbmc-library/__isnanl-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isnanl-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/__isnormalf-01/main.c b/regression/cbmc-library/__isnormalf-01/main.c
deleted file mode 100644
index d21572bc163..00000000000
--- a/regression/cbmc-library/__isnormalf-01/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-01/test.desc b/regression/cbmc-library/__isnormalf-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isnormalf-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/__signbit-01/main.c b/regression/cbmc-library/__signbit-01/main.c
deleted file mode 100644
index e1147fa1a82..00000000000
--- a/regression/cbmc-library/__signbit-01/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-01/test.desc b/regression/cbmc-library/__signbit-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__signbit-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/__signbitf-01/main.c b/regression/cbmc-library/__signbitf-01/main.c
deleted file mode 100644
index a34833282f3..00000000000
--- a/regression/cbmc-library/__signbitf-01/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-01/test.desc b/regression/cbmc-library/__signbitf-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__signbitf-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/_isnan-01/main.c b/regression/cbmc-library/_isnan-01/main.c
deleted file mode 100644
index 039a1ba1707..00000000000
--- a/regression/cbmc-library/_isnan-01/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <float.h>
-
-int main()
-{
-  _isnan();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/_isnan-01/test.desc b/regression/cbmc-library/_isnan-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/_isnan-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/fileno-01/main.c b/regression/cbmc-library/fileno-01/main.c
index c186de1b88d..7820f7ebe28 100644
--- a/regression/cbmc-library/fileno-01/main.c
+++ b/regression/cbmc-library/fileno-01/main.c
@@ -3,14 +3,10 @@
 
 int main()
 {
-  // requires initialization of stdin/stdout/stderr
-  // assert(fileno(stdin) == 0);
-  // assert(fileno(stdout) == 1);
-  // assert(fileno(stderr) == 2);
-
   int fd;
   FILE *some_file = fdopen(fd, "");
-  assert(fileno(some_file) >= -1);
+  if(some_file)
+    assert(fileno(some_file) >= -1);
 
   return 0;
 }
diff --git a/regression/cbmc-library/isfinite-01/main.c b/regression/cbmc-library/isfinite-01/main.c
index 9a739d27435..cb7aeb77c19 100644
--- a/regression/cbmc-library/isfinite-01/main.c
+++ b/regression/cbmc-library/isfinite-01/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-01/test.desc b/regression/cbmc-library/isfinite-01/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/isfinite-01/test.desc
+++ b/regression/cbmc-library/isfinite-01/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-01/main.c b/regression/cbmc-library/isinf-01/main.c
index 37fe2cc5d9e..18b7bb4062c 100644
--- a/regression/cbmc-library/isinf-01/main.c
+++ b/regression/cbmc-library/isinf-01/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-01/main.c b/regression/cbmc-library/isinff-01/main.c
deleted file mode 100644
index 083703644b2..00000000000
--- a/regression/cbmc-library/isinff-01/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-01/test.desc b/regression/cbmc-library/isinff-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/isinff-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/isinfl-01/main.c b/regression/cbmc-library/isinfl-01/main.c
deleted file mode 100644
index f8fcfd36425..00000000000
--- a/regression/cbmc-library/isinfl-01/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-01/test.desc b/regression/cbmc-library/isinfl-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/isinfl-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/isnanf-01/main.c b/regression/cbmc-library/isnanf-01/main.c
deleted file mode 100644
index 34b8ebb4296..00000000000
--- a/regression/cbmc-library/isnanf-01/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-01/test.desc b/regression/cbmc-library/isnanf-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/isnanf-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/isnanl-01/main.c b/regression/cbmc-library/isnanl-01/main.c
deleted file mode 100644
index ef90ee15aa9..00000000000
--- a/regression/cbmc-library/isnanl-01/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-01/test.desc b/regression/cbmc-library/isnanl-01/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/isnanl-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/isnormal-01/main.c b/regression/cbmc-library/isnormal-01/main.c
index d4a976517e3..927306ed586 100644
--- a/regression/cbmc-library/isnormal-01/main.c
+++ b/regression/cbmc-library/isnormal-01/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-01/test.desc b/regression/cbmc-library/isnormal-01/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/isnormal-01/test.desc
+++ b/regression/cbmc-library/isnormal-01/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-01/main.c b/regression/cbmc-library/signbit-01/main.c
index 111356bcd36..6e0858bf1f3 100644
--- a/regression/cbmc-library/signbit-01/main.c
+++ b/regression/cbmc-library/signbit-01/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/regression/cbmc-library/tolower-01/main.c b/regression/cbmc-library/tolower-01/main.c
index 8e528b4a9e1..8568da85a97 100644
--- a/regression/cbmc-library/tolower-01/main.c
+++ b/regression/cbmc-library/tolower-01/main.c
@@ -3,8 +3,12 @@
 
 int main()
 {
+#if !defined(__FreeBSD__) && !defined(__OpenBSD__) && !defined(__NetBSD__)
+  // We would need to model conversion tables, where each of the BSDs has their
+  // peculiar approach.
   int x;
   int r = tolower(x);
   assert(r >= x);
+#endif
   return 0;
 }
diff --git a/regression/cbmc-library/toupper-01/main.c b/regression/cbmc-library/toupper-01/main.c
index 3b98daecf37..f833a8d82d6 100644
--- a/regression/cbmc-library/toupper-01/main.c
+++ b/regression/cbmc-library/toupper-01/main.c
@@ -3,8 +3,12 @@
 
 int main()
 {
+#if !defined(__FreeBSD__) && !defined(__OpenBSD__) && !defined(__NetBSD__)
+  // We would need to model conversion tables, where each of the BSDs has their
+  // peculiar approach.
   int x;
   int r = toupper(x);
   assert(r <= x);
+#endif
   return 0;
 }
diff --git a/regression/contracts-dfcc/variant_multidimensional_ackermann/main.c b/regression/contracts-dfcc/variant_multidimensional_ackermann/main.c
index 7f7e5c1be1f..f8648b9fa56 100644
--- a/regression/contracts-dfcc/variant_multidimensional_ackermann/main.c
+++ b/regression/contracts-dfcc/variant_multidimensional_ackermann/main.c
@@ -8,7 +8,8 @@ int main()
   int n = 5;
   int result = ackermann(m, n);
 
-  printf("Result of the Ackermann function: %d\n", result);
+  // we don't currently have contracts on what printf is assigning to
+  // printf("Result of the Ackermann function: %d\n", result);
   return 0;
 }
 
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 1534260a50e..3f499bbf45a 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -3206,10 +3206,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)
     {
@@ -3225,9 +3226,11 @@ 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")
   {
     if(expr.arguments().size()!=1)
     {
@@ -3243,8 +3246,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(
@@ -3253,7 +3257,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(
@@ -3262,7 +3268,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=
@@ -3295,7 +3303,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)
     {
@@ -3405,10 +3414,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 ac594c0e590..700aaa339f4 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,105 +223,18 @@ 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 */
+/* FUNCTION: __isnormal */
 
-int __builtin_isinf(double d)
+int __isnormal(double d)
 {
-  return __CPROVER_isinfd(d);
-}
-
-/* FUNCTION: __builtin_isinff */
-
-int __builtin_isinff(float f)
-{
-  return __CPROVER_isinff(f);
-}
-
-/* FUNCTION: __builtin_isinf */
-
-int __builtin_isinfl(long double ld)
-{
-  return __CPROVER_isinfld(ld);
-}
-
-/* FUNCTION: __builtin_isnan */
-
-int __builtin_isnan(double d)
-{
-  return __CPROVER_isnand(d);
-}
-
-/* FUNCTION: __builtin_isnanf */
-
-int __builtin_isnanf(float f)
-{
-  return __CPROVER_isnanf(f);
-}
-
-/* FUNCTION: __builtin_huge_valf */
-
-float __builtin_huge_valf(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_huge_val */
-
-double __builtin_huge_val(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
+  return __CPROVER_isnormald(d);
 }
 
-/* FUNCTION: __builtin_huge_vall */
+/* FUNCTION: __isnormall */
 
-long double __builtin_huge_vall(void)
+int __isnormall(long double ld)
 {
-#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
+  return __CPROVER_isnormalld(ld);
 }
 
 /* FUNCTION: _dsign */
@@ -363,7 +283,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);
 }
@@ -3077,8 +3004,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)
@@ -3111,7 +3036,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;
     }
@@ -3120,7 +3045,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))
@@ -3135,9 +3060,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))
@@ -3145,7 +3070,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))
   {
@@ -3225,8 +3150,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)
@@ -3259,7 +3182,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;
     }
@@ -3268,7 +3191,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))
@@ -3283,9 +3206,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))
@@ -3293,7 +3216,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))
   {
@@ -3370,8 +3293,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)
@@ -3404,7 +3325,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;
     }
@@ -3413,7 +3334,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))
@@ -3428,9 +3349,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))
@@ -3438,7 +3359,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))
   {
@@ -3519,8 +3440,6 @@ long double powl(long double x, long double y)
 #  define __CPROVER_FENV_H_INCLUDED
 #endif
 
-double __builtin_inf(void);
-
 double fma(double x, double y, double z)
 {
   // see man fma (https://linux.die.net/man/3/fma)
@@ -3552,7 +3471,7 @@ double fma(double x, double y, double z)
   if(isinf(x_times_y))
   {
     feraiseexcept(FE_OVERFLOW);
-    return __CPROVER_signd(x_times_y) ? -__builtin_inf() : __builtin_inf();
+    return __CPROVER_signd(x_times_y) ? -__CPROVER_inf() : __CPROVER_inf();
   }
   // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
 
@@ -3571,8 +3490,6 @@ double fma(double x, double y, double z)
 #  define __CPROVER_FENV_H_INCLUDED
 #endif
 
-float __builtin_inff(void);
-
 float fmaf(float x, float y, float z)
 {
   // see man fma (https://linux.die.net/man/3/fma)
@@ -3604,7 +3521,7 @@ float fmaf(float x, float y, float z)
   if(isinff(x_times_y))
   {
     feraiseexcept(FE_OVERFLOW);
-    return __CPROVER_signf(x_times_y) ? -__builtin_inff() : __builtin_inff();
+    return __CPROVER_signf(x_times_y) ? -__CPROVER_inff() : __CPROVER_inff();
   }
   // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
 
@@ -3628,8 +3545,6 @@ float fmaf(float x, float y, float z)
 #  define __CPROVER_FLOAT_H_INCLUDED
 #endif
 
-long double __builtin_infl(void);
-
 long double fmal(long double x, long double y, long double z)
 {
   // see man fma (https://linux.die.net/man/3/fma)
@@ -3664,7 +3579,7 @@ long double fmal(long double x, long double y, long double z)
   if(isinfl(x_times_y))
   {
     feraiseexcept(FE_OVERFLOW);
-    return __CPROVER_signld(x_times_y) ? -__builtin_infl() : __builtin_infl();
+    return __CPROVER_signld(x_times_y) ? -__CPROVER_infl() : __CPROVER_infl();
   }
   // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
 
@@ -3691,8 +3606,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
@@ -3720,9 +3633,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))
@@ -3730,7 +3643,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)
   {
@@ -3810,8 +3723,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
@@ -3839,9 +3750,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))
@@ -3849,7 +3760,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)
   {
@@ -3925,7 +3836,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)
@@ -3955,9 +3865,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))
@@ -3965,7 +3875,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/stdio.c b/src/ansi-c/library/stdio.c
index 47a2be1ba6b..bc776cbaa2b 100644
--- a/src/ansi-c/library/stdio.c
+++ b/src/ansi-c/library/stdio.c
@@ -6,15 +6,7 @@
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-/* undefine macros in OpenBSD's stdio.h that are problematic to the checker. */
-#if defined(__OpenBSD__)
-#undef getchar
 #undef putchar
-#undef getc
-#undef feof
-#undef ferror
-#undef fileno
-#endif
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
@@ -237,7 +229,8 @@ __CPROVER_HIDE:;
   __CPROVER_set_must(stream, "closed");
 #endif
   int return_value=__VERIFIER_nondet_int();
-  free(stream);
+  if(stream != stdin && stream != stdout && stream != stderr)
+    free(stream);
   return return_value;
 }
 
@@ -253,25 +246,83 @@ __CPROVER_HIDE:;
 #define __CPROVER_STDLIB_H_INCLUDED
 #endif
 
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
 FILE *fdopen(int handle, const char *mode)
 {
   __CPROVER_HIDE:;
-  (void)handle;
+  if(handle < 0)
+  {
+    errno = EBADF;
+    return NULL;
+  }
   (void)*mode;
 #ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(mode),
     "fdopen zero-termination of 2nd argument");
 #endif
 
-#if !defined(__linux__) || defined(__GLIBC__)
-  FILE *f=malloc(sizeof(FILE));
+#if defined(_WIN32) || defined(__OpenBSD__) || defined(__NetBSD__)
+  switch(handle)
+  {
+  case 0:
+    return stdin;
+  case 1:
+    return stdout;
+  case 2:
+    return stderr;
+  default:
+  {
+    FILE *f = malloc(sizeof(FILE));
+    __CPROVER_assume(fileno(f) == handle);
+    return f;
+  }
+  }
 #else
-  // libraries need to expose the definition of FILE; this is the
+#  if !defined(__linux__) || defined(__GLIBC__)
+  static FILE stdin_file;
+  static FILE stdout_file;
+  static FILE stderr_file;
+#  else
+  // libraries need not expose the definition of FILE; this is the
   // case for musl
-  FILE *f=malloc(sizeof(int));
-#endif
+  static int stdin_file;
+  static int stdout_file;
+  static int stderr_file;
+#  endif
+
+  FILE *f = NULL;
+  switch(handle)
+  {
+  case 0:
+    stdin = &stdin_file;
+    __CPROVER_havoc_object(&stdin_file);
+    f = &stdin_file;
+    break;
+  case 1:
+    stdout = &stdout_file;
+    __CPROVER_havoc_object(&stdout_file);
+    f = &stdout_file;
+    break;
+  case 2:
+    stderr = &stderr_file;
+    __CPROVER_havoc_object(&stderr_file);
+    f = &stderr_file;
+    break;
+  default:
+#  if !defined(__linux__) || defined(__GLIBC__)
+    f = malloc(sizeof(FILE));
+#  else
+    f = malloc(sizeof(int));
+#  endif
+  }
 
+  __CPROVER_assume(fileno(f) == handle);
   return f;
+#endif
 }
 
 /* FUNCTION: _fdopen */
@@ -291,19 +342,60 @@ FILE *fdopen(int handle, const char *mode)
 #define __CPROVER_STDLIB_H_INCLUDED
 #endif
 
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
 #ifdef __APPLE__
+
+#  ifndef LIBRARY_CHECK
+FILE *stdin;
+FILE *stdout;
+FILE *stderr;
+#  endif
+
 FILE *_fdopen(int handle, const char *mode)
 {
   __CPROVER_HIDE:;
-  (void)handle;
+  if(handle < 0)
+  {
+    errno = EBADF;
+    return NULL;
+  }
   (void)*mode;
 #ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(mode),
     "fdopen zero-termination of 2nd argument");
 #endif
 
-  FILE *f=malloc(sizeof(FILE));
+  static FILE stdin_file;
+  static FILE stdout_file;
+  static FILE stderr_file;
+
+  FILE *f = NULL;
+  switch(handle)
+  {
+  case 0:
+    stdin = &stdin_file;
+    __CPROVER_havoc_object(&stdin_file);
+    f = &stdin_file;
+    break;
+  case 1:
+    stdout = &stdout_file;
+    __CPROVER_havoc_object(&stdout_file);
+    f = &stdout_file;
+    break;
+  case 2:
+    stderr = &stderr_file;
+    __CPROVER_havoc_object(&stderr_file);
+    f = &stderr_file;
+    break;
+  default:
+    f = malloc(sizeof(FILE));
+  }
 
+  __CPROVER_assume(fileno(f) == handle);
   return f;
 }
 #endif
@@ -506,6 +598,8 @@ __CPROVER_HIDE:;
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef feof
+
 int __VERIFIER_nondet_int(void);
 
 int feof(FILE *stream)
@@ -538,6 +632,8 @@ int feof(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef ferror
+
 int __VERIFIER_nondet_int(void);
 
 int ferror(FILE *stream)
@@ -570,6 +666,8 @@ int ferror(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef fileno
+
 int __VERIFIER_nondet_int(void);
 
 int fileno(FILE *stream)
@@ -735,6 +833,8 @@ int fgetc(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef getc
+
 int __VERIFIER_nondet_int(void);
 
 int getc(FILE *stream)
@@ -771,6 +871,8 @@ int getc(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef getchar
+
 int __VERIFIER_nondet_int(void);
 
 int getchar(void)
@@ -1939,10 +2041,13 @@ FILE *__acrt_iob_func(unsigned fd)
   switch(fd)
   {
   case 0:
+    __CPROVER_havoc_object(&stdin_file);
     return &stdin_file;
   case 1:
+    __CPROVER_havoc_object(&stdout_file);
     return &stdout_file;
   case 2:
+    __CPROVER_havoc_object(&stderr_file);
     return &stderr_file;
   default:
     return (FILE *)0;
diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh
index 9d973341585..4f14e5e11c4 100755
--- a/src/ansi-c/library_check.sh
+++ b/src/ansi-c/library_check.sh
@@ -36,6 +36,7 @@ perl -p -i -e 's/^_creat\n//' __functions # creat, macOS
 perl -p -i -e 's/^_fcntl\n//' __functions # fcntl, macOS
 perl -p -i -e 's/^_fopen\n//' __functions # fopen, macOS
 perl -p -i -e 's/^_getopt\n//' __functions # getopt, macOS
+perl -p -i -e 's/^_isnan\n//' __functions # isnan, macOS
 perl -p -i -e 's/^_mmap\n//' __functions # mmap, macOS
 perl -p -i -e 's/^_munmap\n//' __functions # mumap, macOS
 perl -p -i -e 's/^_open\n//' __functions # open, macOS
@@ -68,12 +69,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-01/__fgets_chk.desc
 perl -p -i -e 's/^__fprintf_chk\n//' __functions # fprintf-01/__fprintf_chk.desc
 perl -p -i -e 's/^__fread_chk\n//' __functions # fread-01/__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-01/__printf_chk.desc
+perl -p -i -e 's/^__signbit[fl]?\n//' __functions # signbit, __signbitd
 perl -p -i -e 's/^__syslog_chk\n//' __functions # syslog-01/__syslog_chk.desc
 perl -p -i -e 's/^_syslog\$DARWIN_EXTSN\n//' __functions # syslog-01/test.desc
 perl -p -i -e 's/^__time64\n//' __functions # time