tactic_fail_if_not_decided method

Z3_tactic tactic_fail_if_not_decided(Z3_context c)

\brief Return a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains false).

def_API('Z3_tactic_fail_if_not_decided', TACTIC, (_in(CONTEXT),))

Implementation

Z3_tactic tactic_fail_if_not_decided(
  Z3_context c,
) {
  return _tactic_fail_if_not_decided(
    c,
  );
}