[−][src]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.