Tests exhibiting performance problems with floating point equalities

See #4337.

Author: peterschrammel

regression/cbmc/Float-equality1/main.c

@@ -0,0 +1,12 @@
+#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
+}

regression/cbmc/Float-equality1/test_equality.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+-DEQUALITY
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Times out. See #4337.

regression/cbmc/Float-equality1/test_no_equality.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--