tactic_try_for method

Z3_tactic tactic_try_for(
  1. Z3_context c,
  2. Z3_tactic t,
  3. int ms
)

\brief Return a tactic that applies \c t to a given goal for \c ms milliseconds. If \c t does not terminate in \c ms milliseconds, then it fails.

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

Implementation

Z3_tactic tactic_try_for(
  Z3_context c,
  Z3_tactic t,
  int ms,
) {
  return _tactic_try_for(
    c,
    t,
    ms,
  );
}