Opaque functions cause failing override checks

[RustanLeino]

If a method in a trait mentions an opaque function and the overriding method in a class does the same, then the override check still fails:

$ dafny trait-opaque-bug.dfy
Dafny 2.3.0.10506
trait-opaque-bug.dfy(13,9): Error: the method must provide an equal or more permissive precondition than in its parent trait
Execution trace:
    (0,0): anon0

Dafny program verifier finished with 2 verified, 1 error

Method M in the following program gives a repro. A workaround is to wrap the opaque function into another (Workaround below) and mentioning it instead of the original function

predicate {:opaque} P(x: int) {
  x < 5
}

trait Tr {
  method M(x: int)
    requires P(x)
  method N(x: int)
    requires Workaround(x)
}

class C extends Tr {
  method M(x: int)
    requires P(x)
  {
  }
  method N(x: int)
    requires Workaround(x)
  {
  }
}

predicate Workaround(x: int) {
  P(x)
}

The problem comes down to a mismatch of fuel constants, as the following two lines in the generated Boogie code show:

    assume _module.__default.P(StartFuel__module._default.P, x#0);
    assert _module.__default.P(StartFuelAssert__module._default.P, x#0);