fixedpoint_get_reachable method

Z3_ast fixedpoint_get_reachable(
  1. Z3_context c,
  2. Z3_fixedpoint d,
  3. Z3_func_decl pred
)

Retrieve reachable states of a predicate. Note: this functionality is Spacer specific.

def_API('Z3_fixedpoint_get_reachable', AST, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL)))

Implementation

Z3_ast fixedpoint_get_reachable(
  Z3_context c,
  Z3_fixedpoint d,
  Z3_func_decl pred,
) {
  return _fixedpoint_get_reachable(
    c,
    d,
    pred,
  );
}