Skip to main content

check_sat

Function check_sat 

Source
pub unsafe extern "C" fn check_sat(cvc5: *mut Solver) -> Result
Expand description

Check satisfiability.

SMT-LIB:

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

(check-sat)

\endverbatim

@param cvc5 The solver instance. @return The result of the satisfiability check.