Function udiv_zero_condition 

pub(crate) fn udiv_zero_condition(
    numerator: &Expr,
    denominator: &Expr,
) -> BoolExpr

Builds the exact condition for EVM udiv(numerator, denominator) == 0.