Invariant violation due to float in C union when using SMT2 backend

[mgudemann]

CBMC version: cbmc-6.0.0-alpha-81-g0003101480
Operating system: Linux Mint
Exact command line resulting in the issue: cbmc --function f f.c --cvc5
What behaviour did you expect: CBMC analyzes the file using the external CVC5 solver
What happened instead: internal invariant violation when generating the SMT2 problem

With the following program

float f(float f) {
  union U {
    float f;
    int i;
  } u;
  u.f = f;
  assert (u.f == f);
}

CBMC terminates with an invariant violation report when doing the conversion

converting SSA                                 
--- begin invariant violation report ---       
Invariant check failed                         
File: smt2/smt2_conv.cpp:4551 function: flatten2bv                                            
Condition: !use_FPA_theory                     
Reason: floatbv expressions should be flattened when using FPA theory                         
Backtrace:                                     

The problem seems to be that the value of the union should be converted as a floating point bv, but due to the union it is flattened to a bitvector.