From 1d3132ead5377aa62af4030af84534402c095a50 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 24 Oct 2021 17:14:53 +0100
Subject: [PATCH 1/2] Add test for fmod

fmod is notoriously buggy. We are going to fix one case in the
next commit.
---
 regression/cbmc/fmod1/main.c    | 25 +++++++++++++++++++++++++
 regression/cbmc/fmod1/test.desc | 11 +++++++++++
 2 files changed, 36 insertions(+)
 create mode 100644 regression/cbmc/fmod1/main.c
 create mode 100644 regression/cbmc/fmod1/test.desc

diff --git a/regression/cbmc/fmod1/main.c b/regression/cbmc/fmod1/main.c
new file mode 100644
index 00000000000..92416698c6a
--- /dev/null
+++ b/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)));
+}
diff --git a/regression/cbmc/fmod1/test.desc b/regression/cbmc/fmod1/test.desc
new file mode 100644
index 00000000000..76b311da830
--- /dev/null
+++ b/regression/cbmc/fmod1/test.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Currently, the case where the second argument is +-inf is wrongly
+implemented by float_utils.rem.
\ No newline at end of file

From c4deb569e9c431bcde6e05bec68bb1a9fac5f256 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 24 Oct 2021 17:33:04 +0100
Subject: [PATCH 2/2] Fix fmod(x, INFINITY) case

The case where the second argument is +-inf was wrongly
implemented by float_utils.rem.
---
 regression/cbmc/fmod1/test.desc     | 4 +---
 src/solvers/floatbv/float_utils.cpp | 7 +++++--
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/regression/cbmc/fmod1/test.desc b/regression/cbmc/fmod1/test.desc
index 76b311da830..8ebdc8c83ba 100644
--- a/regression/cbmc/fmod1/test.desc
+++ b/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.
\ No newline at end of file
diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp
index d3797a8e387..cd3a246b031 100644
--- a/src/solvers/floatbv/float_utils.cpp
+++ b/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)