[−][src]Function z3_sys::Z3_solver_assert_and_track

pub unsafe extern "C" fn Z3_solver_assert_and_track(
    c: Z3_context, 
    s: Z3_solver, 
    a: Z3_ast, 
    p: Z3_ast
)

Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant 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.

Preconditions:

  • a must be a Boolean expression
  • p must be a Boolean constant (aka variable).

See also: