diff --git a/regression/cbmc/Float-no-simp7/main.c b/regression/cbmc/Float-no-simp7/main.c
new file mode 100644
index 0000000000..c90e60172a
--- /dev/null
+++ b/regression/cbmc/Float-no-simp7/main.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main (int argc, char **argv) {
+  float f =  0x1.9e0c22p-101f;
+  float g = -0x1.3c9014p-50f;
+  float target = -0x1p-149f;
+
+  float result = f * g;
+
+  assert(result == target);
+
+  return 0;
+}
diff --git a/regression/cbmc/Float-no-simp7/test.desc b/regression/cbmc/Float-no-simp7/test.desc
new file mode 100644
index 0000000000..4d2a93e6e2
--- /dev/null
+++ b/regression/cbmc/Float-no-simp7/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--floatbv --no-simplify
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring