Function z3_sys::Z3_mk_solver_for_logic
source · 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
.