mk_fpa_nan method

Z3_ast mk_fpa_nan(Z3_context c, Z3_sort s)

\brief Create a floating-point NaN of sort \c s.

\param c logical context \param s target sort

\sa Z3_mk_fpa_inf \sa Z3_mk_fpa_zero

def_API('Z3_mk_fpa_nan', AST, (_in(CONTEXT),_in(SORT)))

Implementation

Z3_ast mk_fpa_nan(
  Z3_context c,
  Z3_sort s,
) {
  return _mk_fpa_nan(
    c,
    s,
  );
}