solver_check method

int solver_check(Z3_context c, Z3_solver s)

\brief 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 \c Z3_L_TRUE) and model construction is enabled. Note that if the call returns \c 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 \c Z3_L_FALSE).

\sa Z3_solver_check_assumptions

def_API('Z3_solver_check', LBOOL, (_in(CONTEXT), _in(SOLVER)))

Implementation

int solver_check(
  Z3_context c,
  Z3_solver s,
) {
  return _solver_check(
    c,
    s,
  );
}