Function z3_sys::Z3_fixedpoint_add_cover

pub unsafe extern "C" fn Z3_fixedpoint_add_cover(
    c: Z3_context,
    d: Z3_fixedpoint,
    level: c_int,
    pred: Z3_func_decl,
    property: Z3_ast
)

Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forward when possible.

Note: level = -1 is treated as the fixedpoint. So passing -1 for the level means that the property is true of the fixed-point unfolding with respect to pred.

Note: this functionality is PDR specific.