solver_get_proof method

Z3_ast solver_get_proof(
  1. Z3_context c,
  2. Z3_solver s
)

\brief 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 \c Z3_L_FALSE.

def_API('Z3_solver_get_proof', AST, (_in(CONTEXT), _in(SOLVER)))

Implementation

Z3_ast solver_get_proof(
  Z3_context c,
  Z3_solver s,
) {
  return _solver_get_proof(
    c,
    s,
  );
}