mk_real_sort method

Z3_sort mk_real_sort(
  1. Z3_context c
)

\brief Create the real type.

Note that this type is not a floating point number.

def_API('Z3_mk_real_sort', SORT, (_in(CONTEXT), ))

Implementation

Z3_sort mk_real_sort(
  Z3_context c,
) {
  return _mk_real_sort(
    c,
  );
}