parameters: (rm, x, s, ctx=None)
return_statement: return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
docstring: Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
  
      >>> x = FP('x', FPSort(8, 24))
      >>> y = fpToSBV(RTZ(), x, BitVecSort(32))
      >>> print(is_fp(x))
      True
      >>> print(is_bv(y))
      True
      >>> print(is_fp(y))
      False
      >>> print(is_bv(x))
      False
docstring_summary: Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
docstring_tokens: Create a Z3 floating - point conversion expression from floating - point expression to signed bit - vector .
function: def fpToSBV(rm, x, s, ctx=None):
      """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
  
      >>> x = FP('x', FPSort(8, 24))
      >>> y = fpToSBV(RTZ(), x, BitVecSort(32))
      >>> print(is_fp(x))
      True
      >>> print(is_bv(y))
      True
      >>> print(is_fp(y))
      False
      >>> print(is_bv(x))
      False
      """
      if z3_debug():
          _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
          _z3_assert(is_fp(x), "Second argument must be a Z3 floating-point expression")
          _z3_assert(is_bv_sort(s), "Third argument must be Z3 bit-vector sort")
      ctx = _get_ctx(ctx)
      return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
function_tokens: def fpToSBV ( rm , x , s , ctx = None ) : if z3_debug ( ) : _z3_assert ( is_fprm ( rm ) , "First argument must be a Z3 floating-point rounding mode expression" ) _z3_assert ( is_fp ( x ) , "Second argument must be a Z3 floating-point expression" ) _z3_assert ( is_bv_sort ( s ) , "Third argument must be Z3 bit-vector sort" ) ctx = _get_ctx ( ctx ) return BitVecRef ( Z3_mk_fpa_to_sbv ( ctx . ref ( ) , rm . ast , x . ast , s . size ( ) ) , ctx )