Comment 7 for bug 1395019

Meeting
  [-INF, y_6(D) + -1] EQUIVALENCES: { z_5 } (1 elements)
and
  [-INF(OVF), 30]
to
  [-INF(OVF), y_6(D) + -1] EQUIVALENCES: { } (0 elements)
Found new range for z_1: [-INF(OVF), y_6(D) + -1]

is obviously wrong. We run into

  else if ((operand_less_p (*vr0min, vr1max) == 1
            || operand_equal_p (*vr0min, vr1max, 0))
           && operand_less_p (vr1min, *vr0min) == 1)
    {
      /* ( [ ) ] or ( )[ ] */
      if (*vr0type == VR_RANGE
          && vr1type == VR_RANGE)
        *vr0min = vr1min;

where -INF < 30 and -INF(OVF) < -INF. But we have vr0max and vr1max unordered.

Thus we fail to verify that, assuming we've catched this case via

  else if ((maxeq || operand_less_p (vr1max, *vr0max) == 1)
           && (mineq || operand_less_p (*vr0min, vr1min) == 1))
    {
      /* [ ( ) ] or [( ) ] or [ ( )] */
...
  else if ((maxeq || operand_less_p (*vr0max, vr1max) == 1)
           && (mineq || operand_less_p (vr1min, *vr0min) == 1))
    {
      /* ( [ ] ) or ([ ] ) or ( [ ]) */

Fixing that does

Meeting
  [-INF, y_6(D) + -1] EQUIVALENCES: { z_5 } (1 elements)
and
  [-INF(OVF), 30]
to
  VARYING

optimally we'd be able to extract a conservative integer range from
the symbolic range - [-INF, +INF - 1] in this case - and meet them
to [-INF(OVF), +INF - 1] (assuming that y_6 did not overflow).