Skip to main content

cvc5_push

Function cvc5_push 

Source
pub unsafe extern "C" fn cvc5_push(cvc5: *mut Cvc5, nscopes: u32)
Expand description

Push (a) level(s) to the assertion stack.

SMT-LIB:

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

(push <numeral>)

\endverbatim

@param cvc5 The solver instance. @param nscopes The number of levels to push.