Function z3_sys::Z3_fixedpoint_get_cover_delta [] [src]

pub unsafe extern "C" fn Z3_fixedpoint_get_cover_delta(
    c: Z3_context,
    d: Z3_fixedpoint,
    level: c_int,
    pred: Z3_func_decl
) -> Z3_ast

Retrieve the current cover of pred up to level unfoldings. Return just the delta that is known at level. To obtain the full set of properties of pred one should query at level+1 , level+2 etc, and include level=-1.

Note: this functionality is PDR specific.