Function z3_sys::Z3_solver_get_proof

pub unsafe extern "C" fn Z3_solver_get_proof(
    c: Z3_context,
    s: Z3_solver
) -> Z3_ast

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.