Function z3_sys::Z3_goal_precision [−] [src]

pub unsafe extern "C" fn Z3_goal_precision(
    c: Z3_context, 
    g: Z3_goal
) -> GoalPrec

Return the "precision" of the given goal. Goals can be transformed using over and under approximations. A under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.