apply_result_get_subgoal method

Z3_goal apply_result_get_subgoal(
  1. Z3_context c,
  2. Z3_apply_result r,
  3. int i
)

\brief Return one of the subgoals in the \c Z3_apply_result object returned by #Z3_tactic_apply.

\pre i < Z3_apply_result_get_num_subgoals(c, r)

\sa Z3_apply_result_get_num_subgoals

def_API('Z3_apply_result_get_subgoal', GOAL, (_in(CONTEXT), _in(APPLY_RESULT), _in(UINT)))

Implementation

Z3_goal apply_result_get_subgoal(
  Z3_context c,
  Z3_apply_result r,
  int i,
) {
  return _apply_result_get_subgoal(
    c,
    r,
    i,
  );
}