Function z3_sys::Z3_goal_precision

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

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.