Function get_timeout_core_assuming 

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

Get a timeout core of the given assumptions.

This function computes a subset of the given assumptions that cause a timeout when added to the current assertions.

\verbatim embed:rst:leading-asterisk If the result is unknown and the reason is timeout, then the set of assumptions corresponds to a subset of the given assumptions that cause a timeout when added to the current assertions in the specified time :ref:timeout-core-timeout <lbl-option-timeout-core-timeout>. If the result is unsat, then the set of assumptions together with the current assertions correspond to an unsat core for the current assertions. Otherwise, the result is sat, indicating that the given assumptions plus the current assertions are satisfiable, and the returned set of assumptions 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 (<assert>*))

\endverbatim

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

@param cvc5 The solver instance. @param size The number of assumptions. @param assumptions The (non-empty) set of formulas to assume. @param result The resulting result. @param rsize The resulting size of the timeout core.

@return The list of assumptions 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.