mkFpToIEEEBvExpr

Create Fp to IEEE BitVec conversion expression. Converts Fp value to the corresponding IEEE 754-2008 binary format.

Note: conversion is unspecified for NaN values.