Function get_timeout_core 

pub unsafe extern "C" fn get_timeout_core(
    cvc5: *mut Solver,
    result: *mut Result,
    size: *mut usize,
) -> *const Term

Get a timeout core.

\verbatim embed:rst:leading-asterisk This function computes a subset of the current assertions that cause a timeout. It may make multiple checks for satisfiability internally, each limited by the timeout value given by :ref:timeout-core-timeout <lbl-option-timeout-core-timeout>.

If the result is unknown and the reason is timeout, then the list of formulas correspond to a subset of the current assertions that cause a timeout in the specified time :ref:timeout-core-timeout <lbl-option-timeout-core-timeout>. If the result is unsat, then the list of formulas correspond to an unsat core for the current assertions. Otherwise, the result is sat, indicating that the current assertions are satisfiable, and the returned set of assertions is empty. \endverbatim

@note This command does not require being preceeded by a call to cvc5_check_sat().

SMT-LIB:

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

(get-timeout-core)

\endverbatim

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

@param cvc5 The solver instance. @param result The resulting result. @param size The resulting size of the timeout core.

@return The list of assertions determined to be the timeout core. The resulting result is stored in result.

@note The resulting result and term array pointer are only valid until the next call to this function.