Function Z3_mk_simple_solver

pub unsafe extern "C" fn Z3_mk_simple_solver(
    c: Z3_context,
) -> Z3_solver

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

NOTE: 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.

See also:

• Z3_mk_solver
• Z3_mk_solver_for_logic
• Z3_mk_solver_from_tactic