Function udiv_nonzero_condition 

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

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