tactic_repeat method

Z3_tactic tactic_repeat(
  1. Z3_context c,
  2. Z3_tactic t,
  3. int max
)

\brief Return a tactic that keeps applying \c t until the goal is not modified anymore or the maximum number of iterations \c max is reached.

def_API('Z3_tactic_repeat', TACTIC, (_in(CONTEXT), _in(TACTIC), _in(UINT)))

Implementation

Z3_tactic tactic_repeat(
  Z3_context c,
  Z3_tactic t,
  int max,
) {
  return _tactic_repeat(
    c,
    t,
    max,
  );
}