Function z3_sys::Z3_solver_get_proof [−][src]
pub unsafe extern "C" fn Z3_solver_get_proof(
c: Z3_context,
s: Z3_solver
) -> Z3_ast
Expand description
Retrieve the proof for the last Z3_solver_check
or Z3_solver_check_assumptions
The error handler is invoked if proof generation is not enabled,
or if the commands above were not invoked for the given solver,
or if the result was different from Z3_L_FALSE
.