CBMC fails to type-check initialization of static variable of type float with value +INFINITY

[andreast271]

If a static variable inside a function is initialized with +INFINITY, cbmc fails to typecheck the program.
Example program main.c:

#include <math.h>
void func() {
  static float f = +INFINITY;
}

CBMC command: cbmc main.c
Output:

CBMC version 6.7.1 (cbmc-6.7.1-dirty) 64-bit x86_64 linux
Type-checking main
file main.c line 3 function func: expected constant expression, but got '__builtin_inff()'
CONVERSION ERROR

The preprocessor replaces +INFINITY with __builtin_inff(). GCC allows initialization of a static variable with the return value of __builtin_inff(), CBMC does not.