solver_assert_and_track method

void solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p,)

\brief Assert a constraint \c a into the solver, and track it (in the unsat) core using the Boolean constant \c p.

This API is an alternative to #Z3_solver_check_assumptions for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination of the Boolean variables provided using Z3_solver_assert_and_track and the Boolean literals provided using #Z3_solver_check_assumptions.

\pre \c a must be a Boolean expression \pre \c p must be a Boolean constant (aka variable).

\sa Z3_solver_assert \sa Z3_solver_reset

def_API('Z3_solver_assert_and_track', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST), _in(AST)))

Implementation

void solver_assert_and_track(
  Z3_context c,
  Z3_solver s,
  Z3_ast a,
  Z3_ast p,
) {
  return _solver_assert_and_track(
    c,
    s,
    a,
    p,
  );
}