// rhs is guarded against zero. Detector should NOT flag — the path
// predicate inside the if rules out (y == 0).
int divide_guarded(int x, int y) {
    if (y != 0) {
        return x / y;
    }
    return 0;
}