Regression on maintaining assertion in second half of constructors

[robin-aws]

Dafny version

4.10.0

Code to produce this issue

trait Validatable extends object { 

  ghost predicate Valid()
    reads Repr()

  ghost function Repr(): set<object> {
    {}
  }
}

class C {
  constructor (x: Validatable)
    requires x.Valid()
  {
    assert x.Valid();
    new;
    assert x.Valid();  // Fails
  }
}

Command to run and resulting output

% dafny verify regression.dfy
regression.dfy(17,4): Error: assertion might not hold
   |
17 |     assert x.Valid();  // Fails
   |     ^^^^^^

What happened?

Passes on Dafny 4.9.1.

Determined to be caused by this change: #5654

Can be worked around by adding assert unchanged(x.Repr()); before the line that failed.

What type of operating system are you experiencing the problem on?

Mac