fixedpoint_add_cover method

void fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property,)

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

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

Note: this functionality is PDR specific.

def_API('Z3_fixedpoint_add_cover', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(INT), _in(FUNC_DECL), _in(AST)))

Implementation

void fixedpoint_add_cover(
  Z3_context c,
  Z3_fixedpoint d,
  int level,
  Z3_func_decl pred,
  Z3_ast property,
) {
  return _fixedpoint_add_cover(
    c,
    d,
    level,
    pred,
    property,
  );
}