solver_pop method

void solver_pop(
  1. Z3_context c,
  2. Z3_solver s,
  3. int n
)

\brief Backtrack \c n backtracking points.

\sa Z3_solver_get_num_scopes \sa Z3_solver_push

\pre n <= Z3_solver_get_num_scopes(c, s)

def_API('Z3_solver_pop', VOID, (_in(CONTEXT), _in(SOLVER), _in(UINT)))

Implementation

void solver_pop(
  Z3_context c,
  Z3_solver s,
  int n,
) {
  return _solver_pop(
    c,
    s,
    n,
  );
}