Merge pull request #4338 from peterschrammel/floating-point-timeout

Tests exhibiting performance problems with floating point equalities

Author: tautschnig

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

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.

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