Z3_fixedpoint_get_num_levels

z3_sys

Function Z3_fixedpoint_get_num_levels 

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

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.