Conversion Float - Signed Bitvectors
The actual library Float_BV_Converter
in the file ieee_float.mlw
contains only functions to convert a float from (and to) unsigned bitvectors. It would be interesting to also have the same functions for the conversion from (and to) signed bitvectors.
The Smtlib contains a such function:
; from signed machine integer, represented as a 2's complement bit vector
((_ to_fp eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb))