Spurious failure for float to int conversion

[zhassan-aws]

For the following program:

int main() {
  float f = -2147483648;
  int i = (int)f;
  return 0;

The value -2147483648 is the minimum int value and it can be represented in float as confirmed by https://www.h-schmidt.net/FloatConverter/IEEE754.html. Thus, casting it to int should not fail.

$ cbmc f2.c --conversion-check
CBMC version 6.3.1 (cbmc-6.3.1) 64-bit x86_64 linux
Type-checking f2
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is SATISFIABLE

** Results:
f2.c function main
[main.overflow.1] line 3 arithmetic overflow on float to signed integer type conversion in (signed int)f: FAILURE

** 1 of 1 failed (2 iterations)
VERIFICATION FAILED

CBMC version: 6.3.1
Operating system: Ubuntu 20.04
Exact command line resulting in the issue: cbmc f2.c --conversion-check
What behaviour did you expect: Verification successful
What happened instead: Verification failed.