IEEE Floating-point to Bitvector conversion is not supported in Bitwuzla and CVC5, possibly others. The standard says two things about this conversion:

:note
 "There is no function for converting from (_ FloatingPoint eb sb) to the
  corresponding IEEE 754-2008 binary format, as a bit vector (_ BitVec m) with 
  m = eb + sb, because (_ NaN eb sb) has multiple, well-defined representations.
  Instead, an encoding of the kind below is recommended, where f is a term
  of sort (_ FloatingPoint eb sb):

   (declare-fun b () (_ BitVec m))
   (assert (= ((_ to_fp eb sb) b) f))
 "

So it is nice that some solvers give us this method, but in general we can not expect them to add it (for Bitwuzla we asked and got told that it will not be added).

And there is an implementation that we can follow, but it has 2 problems:

• A constraint is created and needs to be added to provers that use this variable (and as far as i can see ONLY those). So we would need to add a constraint without the users knowledge.
• A new BV variable is created that the user also does not know about.

We could of course add a method that returns this info and the constraint as well as the BV variable.

This came up in CPAchecker here.

Also, we already have an implementation in Bitwuzla.

In my opinion, this looks like something a user should add instead of us, but i am completely open to suggestions/ideas.