Fix fmod(x, INFINITY)

regression/cbmc/fmod1/main.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+#include <math.h>
+
+void main()
+{
+  // If x is +-0 and y is not zero, +-0 is returned
+  assert(fmod(0.0, 1.0) == 0.0);
+  assert(fmod(-0.0, 1.0) == -0.0);
+
+  // If x is +-oo and y is not NaN, NaN is returned and FE_INVALID is raised
+  assert(isnan(fmod(INFINITY, 1.0)));
+  assert(isnan(fmod(-INFINITY, 1.0)));
+
+  // If y is +-0 and x is not NaN, NaN is returned and FE_INVALID is raised
+  assert(isnan(fmod(1.0, 0.0)));
+  assert(isnan(fmod(1.0, -0.0)));
+
+  // If y is +-oo and x is finite, x is returned.
+  assert(fmod(1.0, INFINITY) == 1.0);
+  assert(fmod(1.0, -INFINITY) == 1.0);
+
+  // If either argument is NaN, NaN is returned
+  assert(isnan(fmod(1.0, NAN)));
+  assert(isnan(fmod(NAN, 1.0)));
+}

regression/cbmc/fmod1/test.desc

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

src/solvers/floatbv/float_utils.cpp

@@ -547,8 +547,11 @@ bvt float_utilst::rem(const bvt &src1, const bvt &src2)
      We have some approaches that are correct but they really
      don't scale. */
 
-  // stub: do src1-(src1/src2)*src2
-  return sub(src1, mul(div(src1, src2), src2));
+  const unbiased_floatt unpacked2 = unpack(src2);
+
+  // stub: do (src2.infinity ? src1 : (src1/src2)*src2))
+  return bv_utils.select(
+    unpacked2.infinity, src1, sub(src1, mul(div(src1, src2), src2)));
 }
 
 bvt float_utilst::negate(const bvt &src)