Wrong --conversion-check in cast from double to unsigned

[cesaro]

The below program

int main() {
  unsigned u = 0xffffffffu;

  // since the double type seems to be implemented with a IEEE 754 binary64
  // format in CBMC, which has 53 bits of mantissa, double has enough bits to
  // represent the exact value of u, use, e.g., http://weitz.de/ieee/ to check;
  // therefore, C17, section 6.3.1.4, paragraph 2 says that this is
  // defined behavior and d should store the exact value that u stores
  double d = u;

  // defined behavior behavior as well, by C17 section 6.3.1.4, paragraph 1,
  // because the 'unsigned' type can represent the value; however,
  // cbmc --conversion-check complains
  u = (unsigned) d;

  return 0;
}

doesn't have undefined behavior in the double-to-unsigned conversion, according to C17, section 6.3.1.4, paragraph 1, but

cbmc --conversion-check main.c

in Linux, using latest develop, complains about an arithmetic overflow.