Function mk_div_rules 

fn mk_div_rules() -> fn(&[(BaseTy, Expr); N]) -> Option<MatchedRule>

a/b

For unsigned integers, Rust’s truncating division agrees with SMT-LIB’s Euclidean div because both operands are non-negative, so we can emit the exact value T[a/b].

For signed integers, Rust truncates toward zero while SMT-LIB’s div floors (for positive divisors). They only agree when both operands are non-negative, so we use a conditional constraint (same approach as mk_rem_rules for signed integers).