Function z3_sys::Z3_goal_precision [−][src]
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.