fmod/fmodf return 0 for finite operands with a nonzero remainder (fmod(7, 2) gives 0) #9214

I found this issue while reviewing CBMC with AI assistance and reproduced it with cbmc built from the commit below. This report was drafted by AI.

Tested commit: 32441ee (develop); also cbmc 6.11.0. gcc 16.2.1 / glibc for reference.

Reproducer

main.c:

#include <assert.h>
#include <math.h>
#include <stdio.h>

#ifdef __CPROVER__
double nondet_double(void);
#endif

int main(void)
{
#ifdef __CPROVER__
  double x = nondet_double();
  __CPROVER_assume(x == 7.0 || x == 9.0);
#else
  double x = 7.0;
#endif
  double r = fmod(x, 2.0);
  float rf = fmodf((float)x - 1.5f, 2.0f); // fmodf(5.5f, 2.0f)
#ifndef __CPROVER__
  printf("%g %g\n", r, rf);
#endif
  if(x == 7.0)
  {
    assert(r == 1.0);
    assert(rf == 1.5f);
  }
  return 0;
}

x is nondeterministic only so that constant folding does not compute the result.

$ gcc -O0 main.c -o native -lm && ./native
1 1.5
$ cbmc main.c --trace
[main.assertion.1] line 24 assertion r == 1.0: FAILURE
[main.assertion.2] line 25 assertion rf == 1.5f: FAILURE
  r=0.0 (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
  rf=0.0f (00000000 00000000 00000000 00000000)
VERIFICATION FAILED

wrong.c in the reproducer directory asserts the wrong values instead (r == 0.0, rf == 0.0f), and CBMC proves them:

$ cbmc wrong.c
[main.assertion.1] line 24 assertion r == 0.0: SUCCESS
[main.assertion.2] line 25 assertion rf == 0.0f: SUCCESS
VERIFICATION SUCCESSFUL

Expected behavior

C11 7.12.10.1: fmod(x, y) returns x - n*y for the integer n such that the result has the sign of x and magnitude less than |y|. So fmod(7, 2) == 1 and fmodf(5.5f, 2) == 1.5f, as glibc prints.

Actual behavior

Both results are 0 with the default SAT backend. Scope: any C program calling fmod/fmodf/fmodl or __CPROVER_fmod* (the library models at src/ansi-c/library/math.c:1970-2004 call __CPROVER_fmod*). With --z3 the same program hits an invariant violation on floatbv_mod instead. regression/cbmc/fmod1 only tests ±0, ±inf and NaN operands, so it passes; regression/cbmc-library/fmod* are KNOWNBUG placeholders.

Front ends that emit ID_floatbv_mod for a language-level operator are affected the same way. For example, Kani emits it for Rust's float % and proves 7.0 % 2.0 != 1.0 (model-checking/kani#5013).

Cause

__CPROVER_fmod* are typechecked to ID_floatbv_mod (src/ansi-c/c_typecheck_expr.cpp:3355-3376), which boolbvt::convert_floatbv_mod_rem encodes with float_utilst::rem. Its comment (src/solvers/flattening/boolbv_floatbv_mod_rem.cpp:30) says "float_utilst::rem implements lhs-(lhs/rhs)rhs, which matches neither fmod() nor IEEE": 7/2 rounds to 3.5 and 7 - 3.52 = 0. float_utilst::rem (src/solvers/floatbv/float_utils.cpp:702) documents the same limitation.

PR #7885 ("Cleanup fmod vs IEEE remainder") addresses this: it notes that the propositional back-end does not distinguish fmod from IEEE remainder and adds fmod tests. It has been open since 2023-09.

Possibly related: #9204 (the same float_utilst::rem behind fp.rem / __CPROVER_remainder).