To handle this case some SSA implementations add a concept of "pi" nodes, which are used to artificially split variables on branches that establish some useful data flow property.

    x1 = ...
    if (x1 > 0) {
        x2 = pi(x1 & RANGE[1..])
        use(x2)
    } else {
        x3 = pi(x1 & RANGE[..0])
        use(x3)
    }
    x4 = phi(x2, x3) // if used

I have placed the pi nodes in the blocks, but semantically they are placed along the control edge.

Ref e.g. e-SSA in the ABCD value range inference algorithm.