added a test for x>y <=> x-y>0 over floats

Author: Daniel Kroening

regression/cbmc/Float23/main.c

@@ -0,0 +1,5 @@
+int main()
+{
+  float a, b;
+  __CPROVER_assert((a>b)==(a-b>0), "theorem");
+}

regression/cbmc/Float23/test.desc

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