Dafny fails to verify certain inequalities involving subset types unless a variable's definition is inlined into the inequalities

[brady-ds]

Dafny 3.7.3.40719 unexpectedly fails to verify the following code:

type Nonnegative = t: real |
  t >= 0.0

datatype Point = Point(x: Nonnegative, y: Nonnegative)
type ConstrainedPoint = p: Point |
  p.x >= 0.0
  witness Point(0.0, 0.0)

method Bug(point: ConstrainedPoint) {
  var pairs: seq<ConstrainedPoint> := [Point(0.0, point.x)];
  assume pairs[|pairs| - 1].y > point.y > 0.0;
  var ratio := point.y / pairs[0].y;
  assert 0.0 < ratio <= 1.0;
}

reporting assertion might not hold on the assertion at the end of the Bug method. However, the code verifies just fine if the definition of ratio is inlined into the assertion:

type Nonnegative = t: real |
  t >= 0.0

datatype Point = Point(x: Nonnegative, y: Nonnegative)
type ConstrainedPoint = p: Point |
  p.x >= 0.0
  witness Point(0.0, 0.0)

method Bug(point: ConstrainedPoint) {
  var pairs: seq<ConstrainedPoint> := [Point(0.0, point.x)];
  assume pairs[|pairs| - 1].y > point.y > 0.0;
  var ratio := point.y / pairs[0].y;
  assert 0.0 < point.y / pairs[0].y <= 1.0;
}

The bug is strangely fragile. It does not appear if the constraints in the subset types are replaced with true, if the assertion omits either bound, etc. An especially surprising variation is this:

type Nonnegative = t: real |
  t >= 0.0

datatype Point = Point(x: Nonnegative, y: Nonnegative)
type ConstrainedPoint = p: Point |
  p.x >= 0.0
  witness Point(0.0, 0.0)

method Bug(point: ConstrainedPoint) {
  var pairs: seq<ConstrainedPoint> := [Point(0.0, point.x)];
  assume pairs[|pairs| - 1].y > point.y > 0.0;
  var ratio := point.y / pairs[0].y;
  assert 0.0 < ratio;
  assert 0.0 < point.y / pairs[0].y <= 1.0;
}

where now Dafny proves the first assertion but says the second, which it used to be able to show, now might not hold.

[brady-ds]

Linking to #2589 on the off chance that this a duplicate with a different symptom.