diff --git a/regression/cbmc/float-trace/test.c b/regression/cbmc/float-trace/test.c
deleted file mode 100644
index 1f09d8b3ab4..00000000000
--- a/regression/cbmc/float-trace/test.c
+++ /dev/null
@@ -1,28 +0,0 @@
-#include <assert.h>
-#include <math.h>
-#include <stdbool.h>
-
-int main()
-{
-  float fzero = 0.0f;
-  float fone = 1.0f;
-  float fcomplex = 0x1p+37f;
-  float finf = INFINITY;
-  float fnan = NAN;
-
-  double dzero = 0.0;
-  double done = 1.0;
-  double dinf = INFINITY;
-  double dnan = NAN;
-  double dcomplex = -5.56268e-309;
-
-  assert(false);
-
-  return 0;
-}
-
-void test(float value)
-{
-  assert(value == 1.0f);
-  assert(value == 0.0f);
-}
diff --git a/regression/cbmc/float-trace/test.desc b/regression/cbmc/float-trace/test.desc
deleted file mode 100644
index acfd2834cca..00000000000
--- a/regression/cbmc/float-trace/test.desc
+++ /dev/null
@@ -1,32 +0,0 @@
-CORE
-test.c
---trace --xml-ui
-^EXIT=10$
-^SIGNAL=0$
-VERIFICATION FAILED
-<full_lhs>fzero</full_lhs>
-<full_lhs_value binary="0{32}">0.0f</full_lhs_value>
-<full_lhs>fone</full_lhs>
-<full_lhs_value binary="00111111100000000000000000000000">1.0f</full_lhs_value>
-<full_lhs>fcomplex</full_lhs>
-<full_lhs_value binary="01010010000000000000000000000000">1\.374390e\+11f</full_lhs_value>
-<full_lhs>finf</full_lhs>
-<full_lhs_value binary="01{8}0{23}">\+INFINITY</full_lhs_value>
-<full_lhs>fnan</full_lhs>
-<full_lhs_value binary="01{8}[01]*1[01]*">\+NAN</full_lhs_value>
-<full_lhs_value binary="[01]{32}">\+NAN</full_lhs_value>
-<full_lhs>dzero</full_lhs>
-<full_lhs_value binary="0{64}">0.0</full_lhs_value>
-<full_lhs>done</full_lhs>
-<full_lhs_value binary="001{10}0{52}">1.0</full_lhs_value>
-<full_lhs>dcomplex</full_lhs>
-<full_lhs_value binary="1000000000000011111111111111111111000111111100100110011101110111">-5\.562680e-309</full_lhs_value>
-<full_lhs>finf</full_lhs>
-<full_lhs_value binary="01{11}0{52}">\+INFINITY</full_lhs_value>
-<full_lhs>fnan</full_lhs>
-<full_lhs_value binary="01{11}[01]*1[01]*">\+NAN</full_lhs_value>
-<full_lhs_value binary="[01]{64}">\+NAN</full_lhs_value>
---
---
-Checks that the binary value is printed for floating point types
-point types