mk_simple_solver method

Z3_solver mk_simple_solver(Z3_context c)

\brief Create a new incremental solver.

This is equivalent to applying the "smt" tactic.

Unlike #Z3_mk_solver() this solver

• Does not attempt to apply any logic specific tactics.
• Does not change its behaviour based on whether it used incrementally/non-incrementally.

Note that these differences can result in very different performance compared to #Z3_mk_solver().

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. The function #Z3_solver_get_model can also be used even if the result is \c Z3_L_UNDEF, but the returned model is not guaranteed to satisfy quantified assertions.

\remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects. Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.

\sa Z3_mk_solver \sa Z3_mk_solver_for_logic \sa Z3_mk_solver_from_tactic

def_API('Z3_mk_simple_solver', SOLVER, (_in(CONTEXT),))

Implementation

Z3_solver mk_simple_solver(
  Z3_context c,
) {
  return _mk_simple_solver(
    c,
  );
}