Function z3_sys::Z3_fixedpoint_get_num_levels

pub unsafe extern "C" fn Z3_fixedpoint_get_num_levels(
    c: Z3_context,
    d: Z3_fixedpoint,
    pred: Z3_func_decl
) -> c_uint

Query the PDR engine for the maximal levels properties are known about predicate.

This call retrieves the maximal number of relevant unfoldings of pred with respect to the current exploration state. Note: this functionality is PDR specific.