diff --git a/regression/cbmc/Float-equality1/main.c b/regression/cbmc/Float-equality1/main.c
new file mode 100644
index 00000000000..a6d8205d1ab
--- /dev/null
+++ b/regression/cbmc/Float-equality1/main.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+
+void main()
+{
+  double a, b, c;
+  __CPROVER_assume(a + b > c);
+#ifdef EQUALITY
+  double x = a, y = b, z = c;
+  assert(!(z > x + y));
+#else
+  assert(!(c > a + b));
+#endif
+}
diff --git a/regression/cbmc/Float-equality1/test_equality.desc b/regression/cbmc/Float-equality1/test_equality.desc
new file mode 100644
index 00000000000..f9acf6c9c75
--- /dev/null
+++ b/regression/cbmc/Float-equality1/test_equality.desc
@@ -0,0 +1,10 @@
+KNOWNBUG broken-smt-backend
+main.c
+-DEQUALITY
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Times out. See #4337.
diff --git a/regression/cbmc/Float-equality1/test_no_equality.desc b/regression/cbmc/Float-equality1/test_no_equality.desc
new file mode 100644
index 00000000000..fef87fd5cb3
--- /dev/null
+++ b/regression/cbmc/Float-equality1/test_no_equality.desc
@@ -0,0 +1,9 @@
+CORE broken-smt-backend
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--