Function z3_sys::Z3_solver_assert_and_track [−][src]
pub unsafe extern "C" fn Z3_solver_assert_and_track(
c: Z3_context,
s: Z3_solver,
a: Z3_ast,
p: Z3_ast
)
Expand description
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 expressionp
must be a Boolean constant (aka variable).