From b3c9adec0a634f61ed5c5e35fd104c14f525531e Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Thu, 7 Mar 2019 08:39:43 +0000
Subject: [PATCH] Tests exhibiting performance problems with floating point
 equalities

See #4337.
---
 regression/cbmc/Float-equality1/main.c              | 13 +++++++++++++
 regression/cbmc/Float-equality1/test_equality.desc  | 10 ++++++++++
 .../cbmc/Float-equality1/test_no_equality.desc      |  9 +++++++++
 3 files changed, 32 insertions(+)
 create mode 100644 regression/cbmc/Float-equality1/main.c
 create mode 100644 regression/cbmc/Float-equality1/test_equality.desc
 create mode 100644 regression/cbmc/Float-equality1/test_no_equality.desc

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
+--