diff --git a/regression/cbmc-library/Float-div1-refine/main.c b/regression/cbmc-library/Float-div1-refine/main.c
deleted file mode 100644
index 8b05699e4a6..00000000000
--- a/regression/cbmc-library/Float-div1-refine/main.c
+++ /dev/null
@@ -1,53 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-#ifdef __GNUC__
-void inductiveStepHunt(float startState)
-{
-  float target = 0x1.fffffep-3f;
-
-  __CPROVER_assume(
-    (0 < startState) && (fpclassify(startState) == FP_NORMAL) &&
-    (0x1p-126f <= startState));
-
-  float secondPoint = (target / startState);
-
-  float nextState = (startState + secondPoint) / 2;
-
-  float oneAfter = (target / nextState);
-
-  assert(oneAfter > 0);
-}
-
-void simplifiedInductiveStepHunt(float nextState)
-{
-  float target = 0x1.fffffep-3f;
-
-  // Implies nextState == 0x1p+124f;
-  __CPROVER_assume(
-    (0x1.fffffep+123f < nextState) && (nextState < 0x1.000002p+124f));
-
-  float oneAfter = (target / nextState);
-
-  // Is true and correctly proven by constant evaluation
-  // Note that this is the smallest normal number
-  assert(0x1.fffffep-3f / 0x1p+124f == 0x1p-126f);
-
-  assert(oneAfter > 0);
-}
-#endif
-
-int main(void)
-{
-#ifdef __GNUC__
-  //  inductiveStepHunt(0x1p+125f);
-  //  simplifiedInductiveStepHunt(0x1p+124f);
-
-  float f, g;
-
-  inductiveStepHunt(f);
-  simplifiedInductiveStepHunt(g);
-#endif
-
-  return 0;
-}
diff --git a/regression/cbmc-library/Float-div1/main.c b/regression/cbmc-library/Float-div1/main.c
deleted file mode 100644
index 8b05699e4a6..00000000000
--- a/regression/cbmc-library/Float-div1/main.c
+++ /dev/null
@@ -1,53 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-#ifdef __GNUC__
-void inductiveStepHunt(float startState)
-{
-  float target = 0x1.fffffep-3f;
-
-  __CPROVER_assume(
-    (0 < startState) && (fpclassify(startState) == FP_NORMAL) &&
-    (0x1p-126f <= startState));
-
-  float secondPoint = (target / startState);
-
-  float nextState = (startState + secondPoint) / 2;
-
-  float oneAfter = (target / nextState);
-
-  assert(oneAfter > 0);
-}
-
-void simplifiedInductiveStepHunt(float nextState)
-{
-  float target = 0x1.fffffep-3f;
-
-  // Implies nextState == 0x1p+124f;
-  __CPROVER_assume(
-    (0x1.fffffep+123f < nextState) && (nextState < 0x1.000002p+124f));
-
-  float oneAfter = (target / nextState);
-
-  // Is true and correctly proven by constant evaluation
-  // Note that this is the smallest normal number
-  assert(0x1.fffffep-3f / 0x1p+124f == 0x1p-126f);
-
-  assert(oneAfter > 0);
-}
-#endif
-
-int main(void)
-{
-#ifdef __GNUC__
-  //  inductiveStepHunt(0x1p+125f);
-  //  simplifiedInductiveStepHunt(0x1p+124f);
-
-  float f, g;
-
-  inductiveStepHunt(f);
-  simplifiedInductiveStepHunt(g);
-#endif
-
-  return 0;
-}
diff --git a/regression/cbmc-library/Float-no-simp8/main.c b/regression/cbmc-library/Float-no-simp8/main.c
deleted file mode 100644
index 111356bcd36..00000000000
--- a/regression/cbmc-library/Float-no-simp8/main.c
+++ /dev/null
@@ -1,19 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main(int argc, char **argv)
-{
-  float f = -0x1p-129f;
-  float g = 0x1p-129f;
-  float target = 0x0;
-
-  float result = f + g;
-
-  assert(result == target);
-
-#ifndef _MSC_VER
-  assert(signbit(result) == signbit(target));
-#endif
-
-  return 0;
-}
diff --git a/regression/cbmc-library/Float-to-double1/main.c b/regression/cbmc-library/Float-to-double1/main.c
deleted file mode 100644
index b4a09c90936..00000000000
--- a/regression/cbmc-library/Float-to-double1/main.c
+++ /dev/null
@@ -1,19 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-#if defined(_WIN32) && !defined(__CYGWIN__)
-#include <float.h>
-#define isnan _isnan
-#endif
-
-float nondet_float();
-
-int main()
-{
-  float f = nondet_float();
-
-  double d = (double)f;
-  float ff = (float)d;
-
-  assert((f == ff) || (isnan(f) && isnan(ff)));
-}
diff --git a/regression/cbmc-library/Float_lib1/main.c b/regression/cbmc-library/Float_lib1/main.c
deleted file mode 100644
index 7b7ba2981a2..00000000000
--- a/regression/cbmc-library/Float_lib1/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/Float_lib2/main.c b/regression/cbmc-library/Float_lib2/main.c
deleted file mode 100644
index cde01da806f..00000000000
--- a/regression/cbmc-library/Float_lib2/main.c
+++ /dev/null
@@ -1,33 +0,0 @@
-/*
-** largestSubnormalFloat.c
-**
-** Martin Brain
-** martin.brain@cs.ox.ac.uk
-** 25/07/12
-**
-*/
-
-#include <assert.h>
-#include <math.h>
-
-int main(void)
-{
-#ifdef __GNUC__
-  // Visual Studio won't parse the hexadecimal floating-point literal
-  float largestSubnormalFloat = 0x1.fffffcp-127f;
-
-  assert(fpclassify(largestSubnormalFloat) != FP_NAN);
-  assert(fpclassify(largestSubnormalFloat) != FP_INFINITE);
-  assert(fpclassify(largestSubnormalFloat) != FP_ZERO);
-  assert(fpclassify(largestSubnormalFloat) != FP_NORMAL);
-  assert(fpclassify(largestSubnormalFloat) == FP_SUBNORMAL);
-
-  assert(__fpclassifyf(largestSubnormalFloat) == FP_SUBNORMAL);
-
-  char b = __CPROVER_isnormalf(largestSubnormalFloat);
-
-  assert(!b);
-#endif
-
-  return 0;
-}
diff --git a/regression/cbmc-library/Float_lib2/test.desc b/regression/cbmc-library/Float_lib2/test.desc
deleted file mode 100644
index b7d95a28215..00000000000
--- a/regression/cbmc-library/Float_lib2/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/__acrt_iob_func-01/main.c b/regression/cbmc-library/__acrt_iob_func-01/main.c
new file mode 100644
index 00000000000..a58f083a3d7
--- /dev/null
+++ b/regression/cbmc-library/__acrt_iob_func-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <time.h>
+
+int main()
+{
+  __acrt_iob_func();
+  assert(0);
+  return 0;
+}
diff --git a/regression/cbmc-library/Float-no-simp9/test.desc b/regression/cbmc-library/__acrt_iob_func-01/test.desc
similarity index 65%
rename from regression/cbmc-library/Float-no-simp9/test.desc
rename to regression/cbmc-library/__acrt_iob_func-01/test.desc
index 4d2a93e6e26..9542d988e8d 100644
--- a/regression/cbmc-library/Float-no-simp9/test.desc
+++ b/regression/cbmc-library/__acrt_iob_func-01/test.desc
@@ -1,6 +1,6 @@
-CORE
+KNOWNBUG
 main.c
---floatbv --no-simplify
+--pointer-check --bounds-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/__builtin_isinf-01/main.c b/regression/cbmc-library/__builtin_isinf-01/main.c
index 5ad43a85d6f..7b7ba2981a2 100644
--- a/regression/cbmc-library/__builtin_isinf-01/main.c
+++ b/regression/cbmc-library/__builtin_isinf-01/main.c
@@ -1,9 +1,55 @@
 #include <assert.h>
+#include <float.h>
 #include <math.h>
 
 int main()
 {
-  __builtin_isinf();
-  assert(0);
-  return 0;
+  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
index 9542d988e8d..b7d95a28215 100644
--- a/regression/cbmc-library/__builtin_isinf-01/test.desc
+++ b/regression/cbmc-library/__builtin_isinf-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--floatbv
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/__fpclassify-01/main.c b/regression/cbmc-library/__fpclassify-01/main.c
index 2ed68776b6c..8b05699e4a6 100644
--- a/regression/cbmc-library/__fpclassify-01/main.c
+++ b/regression/cbmc-library/__fpclassify-01/main.c
@@ -1,9 +1,53 @@
 #include <assert.h>
 #include <math.h>
 
-int main()
+#ifdef __GNUC__
+void inductiveStepHunt(float startState)
 {
-  __fpclassify();
-  assert(0);
+  float target = 0x1.fffffep-3f;
+
+  __CPROVER_assume(
+    (0 < startState) && (fpclassify(startState) == FP_NORMAL) &&
+    (0x1p-126f <= startState));
+
+  float secondPoint = (target / startState);
+
+  float nextState = (startState + secondPoint) / 2;
+
+  float oneAfter = (target / nextState);
+
+  assert(oneAfter > 0);
+}
+
+void simplifiedInductiveStepHunt(float nextState)
+{
+  float target = 0x1.fffffep-3f;
+
+  // Implies nextState == 0x1p+124f;
+  __CPROVER_assume(
+    (0x1.fffffep+123f < nextState) && (nextState < 0x1.000002p+124f));
+
+  float oneAfter = (target / nextState);
+
+  // Is true and correctly proven by constant evaluation
+  // Note that this is the smallest normal number
+  assert(0x1.fffffep-3f / 0x1p+124f == 0x1p-126f);
+
+  assert(oneAfter > 0);
+}
+#endif
+
+int main(void)
+{
+#ifdef __GNUC__
+  //  inductiveStepHunt(0x1p+125f);
+  //  simplifiedInductiveStepHunt(0x1p+124f);
+
+  float f, g;
+
+  inductiveStepHunt(f);
+  simplifiedInductiveStepHunt(g);
+#endif
+
   return 0;
 }
diff --git a/regression/cbmc-library/Float-div1-refine/test.desc b/regression/cbmc-library/__fpclassify-01/refine.desc
similarity index 100%
rename from regression/cbmc-library/Float-div1-refine/test.desc
rename to regression/cbmc-library/__fpclassify-01/refine.desc
diff --git a/regression/cbmc-library/__fpclassify-01/test.desc b/regression/cbmc-library/__fpclassify-01/test.desc
index 9542d988e8d..b7d95a28215 100644
--- a/regression/cbmc-library/__fpclassify-01/test.desc
+++ b/regression/cbmc-library/__fpclassify-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--floatbv
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/__fpclassifyf-01/main.c b/regression/cbmc-library/__fpclassifyf-01/main.c
index a866b315b86..cde01da806f 100644
--- a/regression/cbmc-library/__fpclassifyf-01/main.c
+++ b/regression/cbmc-library/__fpclassifyf-01/main.c
@@ -1,9 +1,33 @@
+/*
+** largestSubnormalFloat.c
+**
+** Martin Brain
+** martin.brain@cs.ox.ac.uk
+** 25/07/12
+**
+*/
+
 #include <assert.h>
 #include <math.h>
 
-int main()
+int main(void)
 {
-  __fpclassifyf();
-  assert(0);
+#ifdef __GNUC__
+  // Visual Studio won't parse the hexadecimal floating-point literal
+  float largestSubnormalFloat = 0x1.fffffcp-127f;
+
+  assert(fpclassify(largestSubnormalFloat) != FP_NAN);
+  assert(fpclassify(largestSubnormalFloat) != FP_INFINITE);
+  assert(fpclassify(largestSubnormalFloat) != FP_ZERO);
+  assert(fpclassify(largestSubnormalFloat) != FP_NORMAL);
+  assert(fpclassify(largestSubnormalFloat) == FP_SUBNORMAL);
+
+  assert(__fpclassifyf(largestSubnormalFloat) == FP_SUBNORMAL);
+
+  char b = __CPROVER_isnormalf(largestSubnormalFloat);
+
+  assert(!b);
+#endif
+
   return 0;
 }
diff --git a/regression/cbmc-library/__fpclassifyf-01/test.desc b/regression/cbmc-library/__fpclassifyf-01/test.desc
index 9542d988e8d..b7d95a28215 100644
--- a/regression/cbmc-library/__fpclassifyf-01/test.desc
+++ b/regression/cbmc-library/__fpclassifyf-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--floatbv
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/__stdio_common_vfprintf-01/main.c b/regression/cbmc-library/__stdio_common_vfprintf-01/main.c
new file mode 100644
index 00000000000..3147700af82
--- /dev/null
+++ b/regression/cbmc-library/__stdio_common_vfprintf-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <time.h>
+
+int main()
+{
+  __stdio_common_vfprintf();
+  assert(0);
+  return 0;
+}
diff --git a/regression/cbmc-library/Float21/test.desc b/regression/cbmc-library/__stdio_common_vfprintf-01/test.desc
similarity index 65%
rename from regression/cbmc-library/Float21/test.desc
rename to regression/cbmc-library/__stdio_common_vfprintf-01/test.desc
index b7d95a28215..9542d988e8d 100644
--- a/regression/cbmc-library/Float21/test.desc
+++ b/regression/cbmc-library/__stdio_common_vfprintf-01/test.desc
@@ -1,6 +1,6 @@
-CORE
+KNOWNBUG
 main.c
---floatbv
+--pointer-check --bounds-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/errx-01/main.c b/regression/cbmc-library/errx-01/main.c
new file mode 100644
index 00000000000..df515207349
--- /dev/null
+++ b/regression/cbmc-library/errx-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <time.h>
+
+int main()
+{
+  errx();
+  assert(0);
+  return 0;
+}
diff --git a/regression/cbmc-library/errx-01/test.desc b/regression/cbmc-library/errx-01/test.desc
new file mode 100644
index 00000000000..9542d988e8d
--- /dev/null
+++ b/regression/cbmc-library/errx-01/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/int-to-float1/main.c b/regression/cbmc-library/fesetround-04/main.c
similarity index 96%
rename from regression/cbmc-library/int-to-float1/main.c
rename to regression/cbmc-library/fesetround-04/main.c
index 2b9c04ec560..04a85e46e5a 100644
--- a/regression/cbmc-library/int-to-float1/main.c
+++ b/regression/cbmc-library/fesetround-04/main.c
@@ -1,7 +1,7 @@
 #ifdef __GNUC__
 
-#include <assert.h>
-#include <fenv.h>
+#  include <assert.h>
+#  include <fenv.h>
 
 float castWithRounding(int rounding_mode, int value)
 {
@@ -31,7 +31,7 @@ int main(void)
   assert(castWithRounding(FE_TONEAREST, 33554439) == higher);
   assert(castWithRounding(FE_TONEAREST, 33554440) == higher);
 
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   assert(castWithRounding(FE_UPWARD, 33554432) == low);
   assert(castWithRounding(FE_UPWARD, 33554433) == high);
   assert(castWithRounding(FE_UPWARD, 33554434) == high);
@@ -42,9 +42,9 @@ int main(void)
   assert(castWithRounding(FE_UPWARD, -33554434) == -low);
   assert(castWithRounding(FE_UPWARD, -33554435) == -low);
   assert(castWithRounding(FE_UPWARD, -33554436) == -high);
-#endif
+#  endif
 
-#ifdef FE_DOWNWARD
+#  ifdef FE_DOWNWARD
   assert(castWithRounding(FE_DOWNWARD, 33554432) == low);
   assert(castWithRounding(FE_DOWNWARD, 33554433) == low);
   assert(castWithRounding(FE_DOWNWARD, 33554434) == low);
@@ -55,7 +55,7 @@ int main(void)
   assert(castWithRounding(FE_DOWNWARD, -33554434) == -high);
   assert(castWithRounding(FE_DOWNWARD, -33554435) == -high);
   assert(castWithRounding(FE_DOWNWARD, -33554436) == -high);
-#endif
+#  endif
 
   assert(castWithRounding(FE_TOWARDZERO, 33554432) == low);
   assert(castWithRounding(FE_TOWARDZERO, 33554433) == low);
diff --git a/regression/cbmc-library/Double-to-float-with-simp1/test.desc b/regression/cbmc-library/fesetround-04/test.desc
similarity index 100%
rename from regression/cbmc-library/Double-to-float-with-simp1/test.desc
rename to regression/cbmc-library/fesetround-04/test.desc
diff --git a/regression/cbmc-library/int-to-float2/main.c b/regression/cbmc-library/fesetround-05/main.c
similarity index 91%
rename from regression/cbmc-library/int-to-float2/main.c
rename to regression/cbmc-library/fesetround-05/main.c
index a1af415f28f..1e87ae1dba2 100644
--- a/regression/cbmc-library/int-to-float2/main.c
+++ b/regression/cbmc-library/fesetround-05/main.c
@@ -1,6 +1,6 @@
 #ifdef __GNUC__
-#include <assert.h>
-#include <fenv.h>
+#  include <assert.h>
+#  include <fenv.h>
 
 float nondet_float();
 int nondet_int();
@@ -34,15 +34,15 @@ int main(void)
 
   assert((castWithRounding(FE_TONEAREST, x) == high) == (x == 33554435));
 
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   assert(castWithRounding(FE_UPWARD, x) == high);
   assert(castWithRounding(FE_UPWARD, -x) == -low);
-#endif
+#  endif
 
-#ifdef FE_DOWNWARD
+#  ifdef FE_DOWNWARD
   assert(castWithRounding(FE_DOWNWARD, x) == low);
   assert(castWithRounding(FE_DOWNWARD, -x) == -high);
-#endif
+#  endif
 
   assert(castWithRounding(FE_TOWARDZERO, x) == low);
   assert(castWithRounding(FE_TOWARDZERO, -x) == -low);
diff --git a/regression/cbmc-library/Float-div1/test.desc b/regression/cbmc-library/fesetround-05/test.desc
similarity index 100%
rename from regression/cbmc-library/Float-div1/test.desc
rename to regression/cbmc-library/fesetround-05/test.desc
diff --git a/regression/cbmc-library/Float-data-dependent-rounding/main.c b/regression/cbmc-library/fesetround-06/main.c
similarity index 85%
rename from regression/cbmc-library/Float-data-dependent-rounding/main.c
rename to regression/cbmc-library/fesetround-06/main.c
index 07530aaf024..81fb8a71eab 100644
--- a/regression/cbmc-library/Float-data-dependent-rounding/main.c
+++ b/regression/cbmc-library/fesetround-06/main.c
@@ -4,7 +4,7 @@
 #if defined(_MSC_VER) && _MSC_VER < 1800
 // don't have fenv.h
 #else
-#include <fenv.h>
+#  include <fenv.h>
 #endif
 
 int main(void)
@@ -12,8 +12,8 @@ int main(void)
 #if defined(_MSC_VER) && _MSC_VER < 1800
 #else
 
-#ifdef FE_UPWARD
-#ifdef FW_DOWNWARD
+#  ifdef FE_UPWARD
+#    ifdef FW_DOWNWARD
   float f;
   float g;
 
@@ -35,8 +35,8 @@ int main(void)
     float h = f + g;
     assert(h >= f);
   }
-#endif
-#endif
+#    endif
+#  endif
 
 #endif
 
diff --git a/regression/cbmc-library/Float-data-dependent-rounding/test.desc b/regression/cbmc-library/fesetround-06/test.desc
similarity index 100%
rename from regression/cbmc-library/Float-data-dependent-rounding/test.desc
rename to regression/cbmc-library/fesetround-06/test.desc
diff --git a/regression/cbmc-library/Double-to-float-no-simp1-fix1/main.c b/regression/cbmc-library/fesetround-no-simp1-fix1/main.c
similarity index 89%
rename from regression/cbmc-library/Double-to-float-no-simp1-fix1/main.c
rename to regression/cbmc-library/fesetround-no-simp1-fix1/main.c
index 18e6244e7fc..a16946f0366 100644
--- a/regression/cbmc-library/Double-to-float-no-simp1-fix1/main.c
+++ b/regression/cbmc-library/fesetround-no-simp1-fix1/main.c
@@ -1,9 +1,9 @@
 // gcc -Wall -W -lm double-to-float-with-rounding-modes.c -o double-to-float-with-rounding-modes -frounding-math -fsignaling-nans -ffp-contract=off -msse2 -mfpmath=sse
 
 #ifdef __GNUC__
-#include <assert.h>
-#include <fenv.h>
-#include <math.h>
+#  include <assert.h>
+#  include <fenv.h>
+#  include <math.h>
 
 float setRoundingModeAndCast(int mode, double d)
 {
diff --git a/regression/cbmc-library/Double-to-float-no-simp1-fix1/test.desc b/regression/cbmc-library/fesetround-no-simp1-fix1/test.desc
similarity index 100%
rename from regression/cbmc-library/Double-to-float-no-simp1-fix1/test.desc
rename to regression/cbmc-library/fesetround-no-simp1-fix1/test.desc
diff --git a/regression/cbmc-library/Double-to-float-no-simp1-fix2/main.c b/regression/cbmc-library/fesetround-no-simp1-fix2/main.c
similarity index 89%
rename from regression/cbmc-library/Double-to-float-no-simp1-fix2/main.c
rename to regression/cbmc-library/fesetround-no-simp1-fix2/main.c
index f1353c63a36..018cdbc0a89 100644
--- a/regression/cbmc-library/Double-to-float-no-simp1-fix2/main.c
+++ b/regression/cbmc-library/fesetround-no-simp1-fix2/main.c
@@ -1,9 +1,9 @@
 // gcc -Wall -W -lm double-to-float-with-rounding-modes.c -o double-to-float-with-rounding-modes -frounding-math -fsignaling-nans -ffp-contract=off -msse2 -mfpmath=sse
 
 #ifdef __GNUC__
-#include <assert.h>
-#include <fenv.h>
-#include <math.h>
+#  include <assert.h>
+#  include <fenv.h>
+#  include <math.h>
 
 float setRoundingModeAndCast(int mode, double d)
 {
diff --git a/regression/cbmc-library/Double-to-float-no-simp1-fix2/test.desc b/regression/cbmc-library/fesetround-no-simp1-fix2/test.desc
similarity index 100%
rename from regression/cbmc-library/Double-to-float-no-simp1-fix2/test.desc
rename to regression/cbmc-library/fesetround-no-simp1-fix2/test.desc
diff --git a/regression/cbmc-library/Double-to-float-no-simp1/main.c b/regression/cbmc-library/fesetround-no-simp1/main.c
similarity index 81%
rename from regression/cbmc-library/Double-to-float-no-simp1/main.c
rename to regression/cbmc-library/fesetround-no-simp1/main.c
index 13c71047140..8b7145da484 100644
--- a/regression/cbmc-library/Double-to-float-no-simp1/main.c
+++ b/regression/cbmc-library/fesetround-no-simp1/main.c
@@ -1,9 +1,9 @@
 // gcc -Wall -W -lm double-to-float-with-rounding-modes.c -o double-to-float-with-rounding-modes -frounding-math -fsignaling-nans -ffp-contract=off -msse2 -mfpmath=sse
 
 #ifdef __GNUC__
-#include <assert.h>
-#include <fenv.h>
-#include <math.h>
+#  include <assert.h>
+#  include <fenv.h>
+#  include <math.h>
 
 float setRoundingModeAndCast(int mode, double d)
 {
@@ -25,136 +25,136 @@ int main(void)
   // 0x1.fffffep+127f is the largest binary32 float so
   // these should all be representable as floats...
   test(FE_TONEAREST, 0x1.fffffep+127, 0x1.fffffep+127);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, 0x1.fffffep+127, 0x1.fffffep+127);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, 0x1.fffffep+127, 0x1.fffffep+127);
-#endif
+#  endif
   test(FE_TOWARDZERO, 0x1.fffffep+127, 0x1.fffffep+127);
 
   // Likewise, this should be an obvious sanity check
   test(FE_TONEAREST, +INFINITY, +INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, +INFINITY, +INFINITY);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, +INFINITY, +INFINITY);
-#endif
+#  endif
   test(FE_TOWARDZERO, +INFINITY, +INFINITY);
 
   // Nearer to 0x1.fffffep+127 than to 0x1.000000p+128
   test(FE_TONEAREST, 0x1.fffffe0000001p+127, 0x1.fffffep+127);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, 0x1.fffffe0000001p+127, +INFINITY);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, 0x1.fffffe0000001p+127, 0x1.fffffep+127);
-#endif
+#  endif
   test(FE_TOWARDZERO, 0x1.fffffe0000001p+127, 0x1.fffffep+127);
 
   // 0x1.fffffefffffffp+127 is immediately below half way
   test(FE_TONEAREST, 0x1.fffffefffffffp+127, 0x1.fffffep+127);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, 0x1.fffffefffffffp+127, +INFINITY);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, 0x1.fffffefffffffp+127, 0x1.fffffep+127);
-#endif
+#  endif
   test(FE_TOWARDZERO, 0x1.fffffefffffffp+127, 0x1.fffffep+127);
 
   // Half way
   test(FE_TONEAREST, 0x1.ffffffp+127, +INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, 0x1.ffffffp+127, +INFINITY);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, 0x1.ffffffp+127, 0x1.fffffep+127);
-#endif
+#  endif
   test(FE_TOWARDZERO, 0x1.ffffffp+127, 0x1.fffffep+127);
 
   // Larger
   test(FE_TONEAREST, 0x1.0p+128, +INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, 0x1.0p+128, +INFINITY);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, 0x1.0p+128, 0x1.fffffep+127);
-#endif
+#  endif
   test(FE_TOWARDZERO, 0x1.0p+128, 0x1.fffffep+127);
 
   // Huge
   test(FE_TONEAREST, 0x1.fffffffffffffp+1023, +INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, 0x1.fffffffffffffp+1023, +INFINITY);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, 0x1.fffffffffffffp+1023, 0x1.fffffep+127);
-#endif
+#  endif
   test(FE_TOWARDZERO, 0x1.fffffffffffffp+1023, 0x1.fffffep+127);
 
   // Same again but negative
   test(FE_TONEAREST, -0x1.fffffep+127, -0x1.fffffep+127);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, -0x1.fffffep+127, -0x1.fffffep+127);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, -0x1.fffffep+127, -0x1.fffffep+127);
-#endif
+#  endif
   test(FE_TOWARDZERO, -0x1.fffffep+127, -0x1.fffffep+127);
 
   test(FE_TONEAREST, -INFINITY, -INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, -INFINITY, -INFINITY);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, -INFINITY, -INFINITY);
-#endif
+#  endif
   test(FE_TOWARDZERO, -INFINITY, -INFINITY);
 
   test(FE_TONEAREST, -0x1.fffffe0000001p+127, -0x1.fffffep+127);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, -0x1.fffffe0000001p+127, -0x1.fffffep+127);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, -0x1.fffffe0000001p+127, -INFINITY);
-#endif
+#  endif
   test(FE_TOWARDZERO, -0x1.fffffe0000001p+127, -0x1.fffffep+127);
 
   test(FE_TONEAREST, -0x1.fffffefffffffp+127, -0x1.fffffep+127);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, -0x1.fffffefffffffp+127, -0x1.fffffep+127);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, -0x1.fffffefffffffp+127, -INFINITY);
-#endif
+#  endif
   test(FE_TOWARDZERO, -0x1.fffffefffffffp+127, -0x1.fffffep+127);
 
   test(FE_TONEAREST, -0x1.ffffffp+127, -INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, -0x1.ffffffp+127, -0x1.fffffep+127);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, -0x1.ffffffp+127, -INFINITY);
-#endif
+#  endif
   test(FE_TOWARDZERO, -0x1.ffffffp+127, -0x1.fffffep+127);
 
   test(FE_TONEAREST, -0x1.0p+128, -INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, -0x1.0p+128, -0x1.fffffep+127);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, -0x1.0p+128, -INFINITY);
-#endif
+#  endif
   test(FE_TOWARDZERO, -0x1.0p+128, -0x1.fffffep+127);
 
   test(FE_TONEAREST, -0x1.fffffffffffffp+1023, -INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, -0x1.fffffffffffffp+1023, -0x1.fffffep+127);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, -0x1.fffffffffffffp+1023, -INFINITY);
-#endif
+#  endif
   test(FE_TOWARDZERO, -0x1.fffffffffffffp+1023, -0x1.fffffep+127);
 #endif
 
diff --git a/regression/cbmc-library/Double-to-float-no-simp1/test.desc b/regression/cbmc-library/fesetround-no-simp1/test.desc
similarity index 100%
rename from regression/cbmc-library/Double-to-float-no-simp1/test.desc
rename to regression/cbmc-library/fesetround-no-simp1/test.desc
diff --git a/regression/cbmc-library/Double-to-float-with-simp1/main.c b/regression/cbmc-library/fesetround-with-simp1/main.c
similarity index 81%
rename from regression/cbmc-library/Double-to-float-with-simp1/main.c
rename to regression/cbmc-library/fesetround-with-simp1/main.c
index 13c71047140..8b7145da484 100644
--- a/regression/cbmc-library/Double-to-float-with-simp1/main.c
+++ b/regression/cbmc-library/fesetround-with-simp1/main.c
@@ -1,9 +1,9 @@
 // gcc -Wall -W -lm double-to-float-with-rounding-modes.c -o double-to-float-with-rounding-modes -frounding-math -fsignaling-nans -ffp-contract=off -msse2 -mfpmath=sse
 
 #ifdef __GNUC__
-#include <assert.h>
-#include <fenv.h>
-#include <math.h>
+#  include <assert.h>
+#  include <fenv.h>
+#  include <math.h>
 
 float setRoundingModeAndCast(int mode, double d)
 {
@@ -25,136 +25,136 @@ int main(void)
   // 0x1.fffffep+127f is the largest binary32 float so
   // these should all be representable as floats...
   test(FE_TONEAREST, 0x1.fffffep+127, 0x1.fffffep+127);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, 0x1.fffffep+127, 0x1.fffffep+127);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, 0x1.fffffep+127, 0x1.fffffep+127);
-#endif
+#  endif
   test(FE_TOWARDZERO, 0x1.fffffep+127, 0x1.fffffep+127);
 
   // Likewise, this should be an obvious sanity check
   test(FE_TONEAREST, +INFINITY, +INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, +INFINITY, +INFINITY);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, +INFINITY, +INFINITY);
-#endif
+#  endif
   test(FE_TOWARDZERO, +INFINITY, +INFINITY);
 
   // Nearer to 0x1.fffffep+127 than to 0x1.000000p+128
   test(FE_TONEAREST, 0x1.fffffe0000001p+127, 0x1.fffffep+127);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, 0x1.fffffe0000001p+127, +INFINITY);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, 0x1.fffffe0000001p+127, 0x1.fffffep+127);
-#endif
+#  endif
   test(FE_TOWARDZERO, 0x1.fffffe0000001p+127, 0x1.fffffep+127);
 
   // 0x1.fffffefffffffp+127 is immediately below half way
   test(FE_TONEAREST, 0x1.fffffefffffffp+127, 0x1.fffffep+127);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, 0x1.fffffefffffffp+127, +INFINITY);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, 0x1.fffffefffffffp+127, 0x1.fffffep+127);
-#endif
+#  endif
   test(FE_TOWARDZERO, 0x1.fffffefffffffp+127, 0x1.fffffep+127);
 
   // Half way
   test(FE_TONEAREST, 0x1.ffffffp+127, +INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, 0x1.ffffffp+127, +INFINITY);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, 0x1.ffffffp+127, 0x1.fffffep+127);
-#endif
+#  endif
   test(FE_TOWARDZERO, 0x1.ffffffp+127, 0x1.fffffep+127);
 
   // Larger
   test(FE_TONEAREST, 0x1.0p+128, +INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, 0x1.0p+128, +INFINITY);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, 0x1.0p+128, 0x1.fffffep+127);
-#endif
+#  endif
   test(FE_TOWARDZERO, 0x1.0p+128, 0x1.fffffep+127);
 
   // Huge
   test(FE_TONEAREST, 0x1.fffffffffffffp+1023, +INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, 0x1.fffffffffffffp+1023, +INFINITY);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, 0x1.fffffffffffffp+1023, 0x1.fffffep+127);
-#endif
+#  endif
   test(FE_TOWARDZERO, 0x1.fffffffffffffp+1023, 0x1.fffffep+127);
 
   // Same again but negative
   test(FE_TONEAREST, -0x1.fffffep+127, -0x1.fffffep+127);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, -0x1.fffffep+127, -0x1.fffffep+127);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, -0x1.fffffep+127, -0x1.fffffep+127);
-#endif
+#  endif
   test(FE_TOWARDZERO, -0x1.fffffep+127, -0x1.fffffep+127);
 
   test(FE_TONEAREST, -INFINITY, -INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, -INFINITY, -INFINITY);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, -INFINITY, -INFINITY);
-#endif
+#  endif
   test(FE_TOWARDZERO, -INFINITY, -INFINITY);
 
   test(FE_TONEAREST, -0x1.fffffe0000001p+127, -0x1.fffffep+127);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, -0x1.fffffe0000001p+127, -0x1.fffffep+127);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, -0x1.fffffe0000001p+127, -INFINITY);
-#endif
+#  endif
   test(FE_TOWARDZERO, -0x1.fffffe0000001p+127, -0x1.fffffep+127);
 
   test(FE_TONEAREST, -0x1.fffffefffffffp+127, -0x1.fffffep+127);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, -0x1.fffffefffffffp+127, -0x1.fffffep+127);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, -0x1.fffffefffffffp+127, -INFINITY);
-#endif
+#  endif
   test(FE_TOWARDZERO, -0x1.fffffefffffffp+127, -0x1.fffffep+127);
 
   test(FE_TONEAREST, -0x1.ffffffp+127, -INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, -0x1.ffffffp+127, -0x1.fffffep+127);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, -0x1.ffffffp+127, -INFINITY);
-#endif
+#  endif
   test(FE_TOWARDZERO, -0x1.ffffffp+127, -0x1.fffffep+127);
 
   test(FE_TONEAREST, -0x1.0p+128, -INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, -0x1.0p+128, -0x1.fffffep+127);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, -0x1.0p+128, -INFINITY);
-#endif
+#  endif
   test(FE_TOWARDZERO, -0x1.0p+128, -0x1.fffffep+127);
 
   test(FE_TONEAREST, -0x1.fffffffffffffp+1023, -INFINITY);
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   test(FE_UPWARD, -0x1.fffffffffffffp+1023, -0x1.fffffep+127);
-#endif
-#ifdef FE_DOWNWARD
+#  endif
+#  ifdef FE_DOWNWARD
   test(FE_DOWNWARD, -0x1.fffffffffffffp+1023, -INFINITY);
-#endif
+#  endif
   test(FE_TOWARDZERO, -0x1.fffffffffffffp+1023, -0x1.fffffep+127);
 #endif
 
diff --git a/regression/cbmc-library/Float-flags-simp1/test.desc b/regression/cbmc-library/fesetround-with-simp1/test.desc
similarity index 100%
rename from regression/cbmc-library/Float-flags-simp1/test.desc
rename to regression/cbmc-library/fesetround-with-simp1/test.desc
diff --git a/regression/cbmc-library/int-to-float1/test.desc b/regression/cbmc-library/int-to-float1/test.desc
deleted file mode 100644
index b7d95a28215..00000000000
--- a/regression/cbmc-library/int-to-float1/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/int-to-float2/test.desc b/regression/cbmc-library/int-to-float2/test.desc
deleted file mode 100644
index b7d95a28215..00000000000
--- a/regression/cbmc-library/int-to-float2/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/isnan-01/main.c b/regression/cbmc-library/isnan-01/main.c
index 33ffc0bf144..5f7de7da15f 100644
--- a/regression/cbmc-library/isnan-01/main.c
+++ b/regression/cbmc-library/isnan-01/main.c
@@ -1,9 +1,19 @@
 #include <assert.h>
 #include <math.h>
 
+#if defined(_WIN32) && !defined(__CYGWIN__)
+#  include <float.h>
+#  define isnan _isnan
+#endif
+
+float nondet_float();
+
 int main()
 {
-  isnan();
-  assert(0);
-  return 0;
+  float f = nondet_float();
+
+  double d = (double)f;
+  float ff = (float)d;
+
+  assert((f == ff) || (isnan(f) && isnan(ff)));
 }
diff --git a/regression/cbmc-library/isnan-01/test.desc b/regression/cbmc-library/isnan-01/test.desc
index 9542d988e8d..b7d95a28215 100644
--- a/regression/cbmc-library/isnan-01/test.desc
+++ b/regression/cbmc-library/isnan-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--floatbv
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/pthread_getspecific-01/main.c b/regression/cbmc-library/pthread_getspecific-01/main.c
new file mode 100644
index 00000000000..69b727da4e8
--- /dev/null
+++ b/regression/cbmc-library/pthread_getspecific-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <time.h>
+
+int main()
+{
+  pthread_getspecific();
+  assert(0);
+  return 0;
+}
diff --git a/regression/cbmc-library/pthread_getspecific-01/test.desc b/regression/cbmc-library/pthread_getspecific-01/test.desc
new file mode 100644
index 00000000000..9542d988e8d
--- /dev/null
+++ b/regression/cbmc-library/pthread_getspecific-01/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/pthread_key_create-01/main.c b/regression/cbmc-library/pthread_key_create-01/main.c
new file mode 100644
index 00000000000..14995d11d1d
--- /dev/null
+++ b/regression/cbmc-library/pthread_key_create-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <time.h>
+
+int main()
+{
+  pthread_key_create();
+  assert(0);
+  return 0;
+}
diff --git a/regression/cbmc-library/pthread_key_create-01/test.desc b/regression/cbmc-library/pthread_key_create-01/test.desc
new file mode 100644
index 00000000000..9542d988e8d
--- /dev/null
+++ b/regression/cbmc-library/pthread_key_create-01/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/pthread_key_delete-01/main.c b/regression/cbmc-library/pthread_key_delete-01/main.c
new file mode 100644
index 00000000000..d2125c023d2
--- /dev/null
+++ b/regression/cbmc-library/pthread_key_delete-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <time.h>
+
+int main()
+{
+  pthread_key_delete();
+  assert(0);
+  return 0;
+}
diff --git a/regression/cbmc-library/pthread_key_delete-01/test.desc b/regression/cbmc-library/pthread_key_delete-01/test.desc
new file mode 100644
index 00000000000..9542d988e8d
--- /dev/null
+++ b/regression/cbmc-library/pthread_key_delete-01/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/pthread_setspecific-01/main.c b/regression/cbmc-library/pthread_setspecific-01/main.c
new file mode 100644
index 00000000000..0983469811f
--- /dev/null
+++ b/regression/cbmc-library/pthread_setspecific-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <time.h>
+
+int main()
+{
+  pthread_setspecific();
+  assert(0);
+  return 0;
+}
diff --git a/regression/cbmc-library/pthread_setspecific-01/test.desc b/regression/cbmc-library/pthread_setspecific-01/test.desc
new file mode 100644
index 00000000000..9542d988e8d
--- /dev/null
+++ b/regression/cbmc-library/pthread_setspecific-01/test.desc
@@ -0,0 +1,8 @@
+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
index fdfb95d6dac..111356bcd36 100644
--- a/regression/cbmc-library/signbit-01/main.c
+++ b/regression/cbmc-library/signbit-01/main.c
@@ -1,9 +1,19 @@
 #include <assert.h>
 #include <math.h>
 
-int main()
+int main(int argc, char **argv)
 {
-  signbit();
-  assert(0);
+  float f = -0x1p-129f;
+  float g = 0x1p-129f;
+  float target = 0x0;
+
+  float result = f + g;
+
+  assert(result == target);
+
+#ifndef _MSC_VER
+  assert(signbit(result) == signbit(target));
+#endif
+
   return 0;
 }
diff --git a/regression/cbmc-library/signbit-01/test.desc b/regression/cbmc-library/signbit-01/test.desc
index 9542d988e8d..4d2a93e6e26 100644
--- a/regression/cbmc-library/signbit-01/test.desc
+++ b/regression/cbmc-library/signbit-01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+--floatbv --no-simplify
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/string-abstraction/test-c-with-string-abstraction.desc b/regression/cbmc-library/strlen-02/test-c-with-string-abstraction.desc
similarity index 100%
rename from regression/cbmc-library/string-abstraction/test-c-with-string-abstraction.desc
rename to regression/cbmc-library/strlen-02/test-c-with-string-abstraction.desc
diff --git a/regression/cbmc-library/string-abstraction/test-c-without-string-abstraction.desc b/regression/cbmc-library/strlen-02/test-c-without-string-abstraction.desc
similarity index 100%
rename from regression/cbmc-library/string-abstraction/test-c-without-string-abstraction.desc
rename to regression/cbmc-library/strlen-02/test-c-without-string-abstraction.desc
diff --git a/regression/cbmc-library/string-abstraction/test.c b/regression/cbmc-library/strlen-02/test.c
similarity index 100%
rename from regression/cbmc-library/string-abstraction/test.c
rename to regression/cbmc-library/strlen-02/test.c
diff --git a/regression/cbmc-library/Float-flags-no-simp1/main.c b/regression/cbmc/Float-flags-no-simp1/main.c
similarity index 100%
rename from regression/cbmc-library/Float-flags-no-simp1/main.c
rename to regression/cbmc/Float-flags-no-simp1/main.c
diff --git a/regression/cbmc-library/Float-flags-no-simp1/test.desc b/regression/cbmc/Float-flags-no-simp1/test.desc
similarity index 71%
rename from regression/cbmc-library/Float-flags-no-simp1/test.desc
rename to regression/cbmc/Float-flags-no-simp1/test.desc
index 4d2a93e6e26..94662a50f80 100644
--- a/regression/cbmc-library/Float-flags-no-simp1/test.desc
+++ b/regression/cbmc/Float-flags-no-simp1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend thorough-paths
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc-library/Float-flags-simp1/main.c b/regression/cbmc/Float-flags-simp1/main.c
similarity index 100%
rename from regression/cbmc-library/Float-flags-simp1/main.c
rename to regression/cbmc/Float-flags-simp1/main.c
diff --git a/regression/cbmc-library/Float_lib1/test.desc b/regression/cbmc/Float-flags-simp1/test.desc
similarity index 72%
rename from regression/cbmc-library/Float_lib1/test.desc
rename to regression/cbmc/Float-flags-simp1/test.desc
index b7d95a28215..6a6096cf927 100644
--- a/regression/cbmc-library/Float_lib1/test.desc
+++ b/regression/cbmc/Float-flags-simp1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-cprover-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc-library/Float-no-simp9/main.c b/regression/cbmc/Float-no-simp9/main.c
similarity index 94%
rename from regression/cbmc-library/Float-no-simp9/main.c
rename to regression/cbmc/Float-no-simp9/main.c
index 50770871f37..93624d521d4 100644
--- a/regression/cbmc-library/Float-no-simp9/main.c
+++ b/regression/cbmc/Float-no-simp9/main.c
@@ -2,7 +2,7 @@
 #include <math.h>
 
 #ifndef _MSC_VER
-#include <fenv.h>
+#  include <fenv.h>
 #endif
 
 void testAdd(int mode, double f, double g, int sign)
@@ -40,19 +40,19 @@ int main(int argc, char **argv)
   testAdd(FE_TONEAREST, plusZero, minusZero, 0);
   testAdd(FE_TONEAREST, var, -var, 0);
 
-#ifdef FE_UPWARD
+#  ifdef FE_UPWARD
   testAdd(FE_UPWARD, plusZero, plusZero, 0);
   testAdd(FE_UPWARD, minusZero, minusZero, 1);
   testAdd(FE_UPWARD, plusZero, minusZero, 0);
   testAdd(FE_UPWARD, var, -var, 0);
-#endif
+#  endif
 
-#ifdef FE_DOWNWARD
+#  ifdef FE_DOWNWARD
   testAdd(FE_DOWNWARD, plusZero, plusZero, 0);
   testAdd(FE_DOWNWARD, minusZero, minusZero, 1);
   testAdd(FE_DOWNWARD, plusZero, minusZero, 1);
   testAdd(FE_DOWNWARD, var, -var, 1);
-#endif
+#  endif
 
   testAdd(FE_TOWARDZERO, plusZero, plusZero, 0);
   testAdd(FE_TOWARDZERO, minusZero, minusZero, 1);
diff --git a/regression/cbmc-library/Float-no-simp8/test.desc b/regression/cbmc/Float-no-simp9/test.desc
similarity index 71%
rename from regression/cbmc-library/Float-no-simp8/test.desc
rename to regression/cbmc/Float-no-simp9/test.desc
index 4d2a93e6e26..94662a50f80 100644
--- a/regression/cbmc-library/Float-no-simp8/test.desc
+++ b/regression/cbmc/Float-no-simp9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend thorough-paths
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc-library/Float21/main.c b/regression/cbmc/Float21/main.c
similarity index 100%
rename from regression/cbmc-library/Float21/main.c
rename to regression/cbmc/Float21/main.c
diff --git a/regression/cbmc-library/Float-to-double1/test.desc b/regression/cbmc/Float21/test.desc
similarity index 100%
rename from regression/cbmc-library/Float-to-double1/test.desc
rename to regression/cbmc/Float21/test.desc
diff --git a/regression/cbmc-library/float-nan-check/main.c b/regression/cbmc/float-nan-check/main.c
similarity index 98%
rename from regression/cbmc-library/float-nan-check/main.c
rename to regression/cbmc/float-nan-check/main.c
index 23e7441cae2..66d39556905 100644
--- a/regression/cbmc-library/float-nan-check/main.c
+++ b/regression/cbmc/float-nan-check/main.c
@@ -10,7 +10,8 @@
 // generated because one of the values is already NaN the assertion is not
 // produced.
 
-union container {
+union container
+{
   uint32_t u;
   float f;
 };
diff --git a/regression/cbmc-library/float-nan-check/test.desc b/regression/cbmc/float-nan-check/test.desc
similarity index 100%
rename from regression/cbmc-library/float-nan-check/test.desc
rename to regression/cbmc/float-nan-check/test.desc
diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh
index 0d2d62e56df..c73fa8b1db7 100755
--- a/src/ansi-c/library_check.sh
+++ b/src/ansi-c/library_check.sh
@@ -19,3 +19,65 @@ for f in "$@"; do
     rm __libcheck.s __libcheck.i __libcheck.c
     [ "${ec}" -eq 0 ] || exit "${ec}"
 done
+
+# Make sure all internal library functions have tests exercising them:
+grep '^/\* FUNCTION:' ../*/library/* | cut -f3 -d" " | sort -u > __functions
+
+# Some functions are not expected to have tests:
+perl -p -i -e 's/^__CPROVER_jsa_synthesise\n//' __functions
+perl -p -i -e 's/^java::java.io.InputStream.read:\(\)I\n//' __functions
+perl -p -i -e 's/^__CPROVER_contracts_library\n//' __functions
+
+# Some functions are implicitly covered by running on different operating
+# systems:
+perl -p -i -e 's/^_fopen\n//' __functions # fopen, 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/^_pipe\n//' __functions # pipe, macOS
+perl -p -i -e 's/^_setjmp\n//' __functions # pipe, macOS
+perl -p -i -e 's/^_time(32|64)\n//' __functions # time, Windows
+perl -p -i -e 's/^__isoc99_v?fscanf\n//' __functions # fscanf, Linux
+perl -p -i -e 's/^__isoc99_v?scanf\n//' __functions # scanf, Linux
+perl -p -i -e 's/^__isoc99_v?sscanf\n//' __functions # sscanf, Linux
+perl -p -i -e 's/^__sigsetjmp\n//' __functions # sigsetjmp, Linux
+perl -p -i -e 's/^__stdio_common_vfscanf\n//' __functions # fscanf, Windows
+perl -p -i -e 's/^__stdio_common_vsscanf\n//' __functions # sscanf, Windows
+
+# Some functions are covered by existing tests:
+perl -p -i -e 's/^__CPROVER_deallocate\n//' __functions # free-01
+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/^munmap\n//' __functions # mmap-01
+
+# Some functions are covered by tests in other folders:
+perl -p -i -e 's/^__spawned_thread\n//' __functions # any pthread_create tests
+perl -p -i -e 's/^__builtin_ffsl?l?\n//' __functions # cbmc/__builtin_ffs-01
+perl -p -i -e 's/^__builtin_[su]addl?l?_overflow\n//' __functions # cbmc/gcc_builtin_add_overflow
+perl -p -i -e 's/^__builtin_[su]mull?l?_overflow\n//' __functions # cbmc/gcc_builtin_mul_overflow
+perl -p -i -e 's/^__builtin_[su]subl?l?_overflow\n//' __functions # cbmc/gcc_builtin_sub_overflow
+perl -p -i -e 's/^__builtin_ia32_p(add|sub)sw\n//' __functions # cbmc/SIMD1
+perl -p -i -e 's/^__builtin_ia32_psubu?sw128\n//' __functions # cbmc/SIMD1
+perl -p -i -e 's/^__builtin_ia32_vec_ext_v16qi\n//' __functions # cbmc/SIMD1
+perl -p -i -e 's/^__builtin_ia32_vec_ext_v2di\n//' __functions # cbmc/SIMD1
+perl -p -i -e 's/^__builtin_ia32_vec_ext_v4s[fi]\n//' __functions # cbmc/SIMD1
+perl -p -i -e 's/^__builtin_ia32_vec_ext_v[48]hi\n//' __functions # cbmc/SIMD1
+perl -p -i -e 's/^__builtin_ia32_vec_init_v4hi\n//' __functions # cbmc/SIMD1
+perl -p -i -e 's/^_mm_adds_ep[iu]16\n//' __functions # cbmc/SIMD1
+perl -p -i -e 's/^_mm_extract_epi(16|32)\n//' __functions # cbmc/SIMD1
+perl -p -i -e 's/^_mm_extract_pi16\n//' __functions # cbmc/SIMD1
+perl -p -i -e 's/^_mm_set_epi(16|32)\n//' __functions # cbmc/SIMD1
+perl -p -i -e 's/^_mm_set_pi16\n//' __functions # cbmc/SIMD1
+perl -p -i -e 's/^_mm_setr_epi(16|32)\n//' __functions # cbmc/SIMD1
+perl -p -i -e 's/^_mm_setr_pi16\n//' __functions # cbmc/SIMD1
+perl -p -i -e 's/^_mm_subs_ep[iu]16\n//' __functions # cbmc/SIMD1
+
+ls ../../regression/cbmc-library/ | grep -- - | cut -f1 -d- | sort -u > __tests
+diff -u __tests __functions
+ec="${?}"
+rm __functions __tests
+if [ $ec != 0 ]; then
+  echo "Tests and library functions don't match."
+  echo "Lines prefixed with - are tests not matching any library function."
+  echo "Lines prefixed with + are functions lacking a test."
+fi
+exit "${ec}"