Function get_proof 

pub unsafe extern "C" fn get_proof(
    cvc5: *mut Solver,
    c: ProofComponent,
    size: *mut usize,
) -> *const Proof

Get a proof associated with the most recent call to checkSat.

SMT-LIB:

\verbatim embed:rst:leading-asterisk .. code:: smtlib

(get-proof :c)

Requires to enable option :ref:produce-proofs <lbl-option-produce-proofs>. The string representation depends on the value of option :ref:produce-proofs <lbl-option-proof-format-mode>. \endverbatim

@warning This function is experimental and may change in future versions.

@param cvc5 The solver instance. @param c The component of the proof to return @param size The size of the resulting array of proofs. @return An array of proofs.

@note The returned Cvc5Proof array pointer is only valid until the next call to this function.