Function z3_sys::Z3_mk_goal

pub unsafe extern "C" fn Z3_mk_goal(
    c: Z3_context,
    models: Z3_bool,
    unsat_cores: Z3_bool,
    proofs: Z3_bool
) -> Z3_goal

Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.

If models == true, then model generation is enabled for the new goal.

If unsat_cores == true, then unsat core generation is enabled for the new goal.

If proofs == true, then proof generation is enabled for the new goal.

NOTE: The Z3 context c must have been created with proof generation support.

NOTE: Reference counting must be used to manage goals, even when the Z3_context was created using Z3_mk_context instead of Z3_mk_context_rc.