Divide by +INFINITY raises NaN failure with --nan-check even when numerator is a finite number

[sree314]

On both CBMC 6.4 and CBMC 5.48, CBMC's --nan-check raises a NaN error when a finite float is divided by +INFINITY. Per my reading of the standard, this should not signal an exception:

I'm reading Section 6.1 of IEEE 754-2019, "Infinity Arithmetic", I quote:

Operations on infinite operands are usually exact and therefore signal no exceptions, including, among others
[snip]
-- division(∞, x) or division(x, ∞) for finite x

#include <assert.h>
#include <math.h>
union FloatInt {
    float f;
    unsigned int i;
};

int main(void) {
   union FloatInt a, b;

   a.i = 1065353216;  // 1.0
   b.i = 2139095040; // +INF
   float c = a.f / b.f;
  return 0;
}

Run as cbmc --trace --nan-check /tmp/testdiv.c, CBMC 6.4 returns:

CBMC version 6.4.0 (cbmc-6.4.0) 64-bit x86_64 linux
Type-checking testdiv
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
Building error trace

** Results:
/tmp/testdiv.c function main
[main.NaN.1] line 15 NaN on / in byte_extract_little_endian(a, 0l, float) / byte_extract_little_endian(b, 0l, float): FAILURE

Trace for main.NaN.1:

State 11 file /tmp/testdiv.c function main line 11 thread 0
----------------------------------------------------
  a={ .f=0.0f } (00000000 00000000 00000000 00000000)

State 12 file /tmp/testdiv.c function main line 11 thread 0
----------------------------------------------------
  b={ .f=0.0f } (00000000 00000000 00000000 00000000)

State 13 file /tmp/testdiv.c function main line 13 thread 0
----------------------------------------------------
  a.i=1065353216u (00111111 10000000 00000000 00000000)

State 14 file /tmp/testdiv.c function main line 13 thread 0
----------------------------------------------------
  a.f=1.0f (00111111 10000000 00000000 00000000)

State 15 file /tmp/testdiv.c function main line 13 thread 0
----------------------------------------------------
  a.i=1065353216u (00111111 10000000 00000000 00000000)

State 16 file /tmp/testdiv.c function main line 14 thread 0
----------------------------------------------------
  b.i=2139095040u (01111111 10000000 00000000 00000000)

State 17 file /tmp/testdiv.c function main line 14 thread 0
----------------------------------------------------
  b.f=+INFINITY (01111111 10000000 00000000 00000000)

State 18 file /tmp/testdiv.c function main line 14 thread 0
----------------------------------------------------
  b.i=2139095040u (01111111 10000000 00000000 00000000)

Violated property:
  file /tmp/testdiv.c function main line 15 thread 0
  NaN on / in byte_extract_little_endian(a, 0l, float) / byte_extract_little_endian(b, 0l, float)
  (!IEEE_FLOAT_EQUAL(a.f, 0.0f) || !IEEE_FLOAT_EQUAL(b.f, 0.0f)) && !isinf(b.f)



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

Note the union is not the issue, the problem also replicates with:

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

int main(void) {
   float a, b;

   a = 1.0;  // 1.0
   b = INFINITY; 
   float c = a / b;
  return 0;
}

Trace:

CBMC version 6.4.0 (cbmc-6.4.0) 64-bit x86_64 linux
Type-checking testdiv2
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
Building error trace

** Results:
/tmp/testdiv2.c function main
[main.NaN.1] line 9 NaN on / in a / b: FAILURE

Trace for main.NaN.1:

State 11 file /tmp/testdiv2.c function main line 5 thread 0
----------------------------------------------------
  a=0.0f (00000000 00000000 00000000 00000000)

State 12 file /tmp/testdiv2.c function main line 5 thread 0
----------------------------------------------------
  b=0.0f (00000000 00000000 00000000 00000000)

State 13 file /tmp/testdiv2.c function main line 7 thread 0
----------------------------------------------------
  a=1.0f (00111111 10000000 00000000 00000000)

State 16 file <builtin-library-__builtin_inff> function __builtin_inff line 7 thread 0
----------------------------------------------------
  goto_symex$$return_value$$__builtin_inff=+INFINITY (01111111 10000000 00000000 00000000)

State 18 file /tmp/testdiv2.c function main line 8 thread 0
----------------------------------------------------
  b=+INFINITY (01111111 10000000 00000000 00000000)

Violated property:
  file /tmp/testdiv2.c function main line 9 thread 0
  NaN on / in a / b
  (!IEEE_FLOAT_EQUAL(a, 0.0f) || !IEEE_FLOAT_EQUAL(b, 0.0f)) && !isinf(b)



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