Fix fmod(x, INFINITY) case

The case where the second argument is +-inf was wrongly
implemented by float_utils.rem.

Author: peterschrammel

regression/cbmc/fmod1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE broken-z3-smt-backend broken-smt-backend
 main.c
 
 ^EXIT=0$
@@ -7,5 +7,3 @@ main.c
 --
 ^warning: ignoring
 --
-Currently, the case where the second argument is +-inf is wrongly
-implemented by float_utils.rem.

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)