Regression in floating-point floor

[zhassan-aws]

For the following C program:

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

int main() {
    float f = -42.6;
    float g = floorf(f);
    assert(g == -43.0);
    return 0;
}

verification fails with the latest commit (0fc8a49):

$ cbmc --version
6.4.1 (cbmc-6.4.1-159-g0fc8a492c8)
$ cbmc ffl.c 
CBMC version 6.4.1 (cbmc-6.4.1-159-g0fc8a492c8) 64-bit x86_64 linux
Type-checking ffl
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:
ffl.c function main
[main.assertion.1] line 7 assertion g == -43.0: FAILURE

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

which is an incorrect.

The program correctly passes with CBMC 6.4.1:

$ cbmc --version
6.4.1 (cbmc-6.4.1)
$ cbmc ffl.c 
CBMC version 6.4.1 (cbmc-6.4.1-159-g0fc8a492c8) 64-bit x86_64 linux
Type-checking ffl
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:
ffl.c function main
[main.assertion.1] line 7 assertion g == -43.0: FAILURE

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