pub unsafe extern "C" fn Z3_apply_result_convert_model(
    c: Z3_context,
    r: Z3_apply_result,
    i: c_uint,
    m: Z3_model
) -> Z3_model
Expand description

Convert a model for the subgoal Z3_apply_result_get_subgoal(c, r, i) into a model for the original goal g. Where g is the goal used to create r using Z3_tactic_apply(c, t, g).