fixedpoint_add_invariant method

void fixedpoint_add_invariant(
  1. Z3_context c,
  2. Z3_fixedpoint d,
  3. Z3_func_decl pred,
  4. Z3_ast property,
)

\brief Add an invariant for the predicate \c pred. Add an assumed invariant of predicate \c pred.

Note: this functionality is Spacer specific.

def_API('Z3_fixedpoint_add_invariant', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL), _in(AST)))

Implementation

void fixedpoint_add_invariant(
  Z3_context c,
  Z3_fixedpoint d,
  Z3_func_decl pred,
  Z3_ast property,
) {
  return _fixedpoint_add_invariant(
    c,
    d,
    pred,
    property,
  );
}