rcf_mk_infinitesimal method

Z3_rcf_num rcf_mk_infinitesimal(
  1. Z3_context c
)

\brief Return a new infinitesimal that is smaller than all elements in the Z3 field.

def_API('Z3_rcf_mk_infinitesimal', RCF_NUM, (_in(CONTEXT),))

Implementation

Z3_rcf_num rcf_mk_infinitesimal(
  Z3_context c,
) {
  return _rcf_mk_infinitesimal(
    c,
  );
}