Function z3_sys::Z3_solver_check

pub unsafe extern "C" fn Z3_solver_check(
    c: Z3_context,
    s: Z3_solver
) -> Z3_lbool

Check whether the assertions in a given solver are consistent or not.

The function Z3_solver_get_model retrieves a model if the assertions is satisfiable (i.e., the result is Z3_L_TRUE) and model construction is enabled. Note that if the call returns Z3_L_UNDEF, Z3 does not ensure that calls to Z3_solver_get_model succeed and any models produced in this case are not guaranteed to satisfy the assertions.

The function Z3_solver_get_proof retrieves a proof if proof generation was enabled when the context was created, and the assertions are unsatisfiable (i.e., the result is Z3_L_FALSE).

See also:

• Z3_solver_check_assumptions