Skip to main content

get_assertions

Function get_assertions 

Source
pub unsafe extern "C" fn get_assertions(
    cvc5: *mut Solver,
    size: *mut usize,
) -> *const Term
Expand description

Get the list of asserted formulas.

SMT-LIB:

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

(get-assertions)

\endverbatim

@param cvc5 The solver instance. @param size The size of the resulting assertions array. @return The list of asserted formulas. @note The returned Cvc5Term array pointer is only valid until the next call to this function.