Function z3_sys::Z3_mk_solver_for_logic[][src]

pub unsafe extern "C" fn Z3_mk_solver_for_logic(
    c: Z3_context,
    logic: Z3_symbol
) -> Z3_solver
Expand description

Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unknown or unsupported.

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.