Function goal_to_negated_constraint 

pub fn goal_to_negated_constraint(
    rel: &str,
    lhs: &IntExpr,
    rhs: &IntExpr,
) -> Option<IntConstraint>

Convert a goal to constraints for validity checking using integer semantics.

Key difference from lia: strict inequalities are converted for integers.

• x < k becomes x <= k - 1 (since x must be an integer)
• x > k becomes x >= k + 1

To prove a goal is valid, we check if its negation is unsatisfiable.