You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
: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))"
The text was updated successfully, but these errors were encountered:
Possible solution from smt-lib:
The text was updated successfully, but these errors were encountered: