cannot prove simple facts about functions with opaque read clauses

[tjhance]

This code:

method methodNotModifyingAnything()
{
}

class M {
  var x: int;
}

function {:opaque} OpaqueFunc(m: M) : set<object>
{
  { m }
}

predicate {:opaque} foo(m: M)
reads m
reads OpaqueFunc(m)
{
  m.x == 5
}

method f(m: M)
requires foo(m);
ensures foo(m);
{
  methodNotModifyingAnything();
}

Gives this error:

$ dafny a.dfy
Dafny 2.3.0.10506
a.dfy(24,0): Error BP5003: A postcondition might not hold on this return path.
a.dfy(23,8): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0

Dafny program verifier finished with 1 verified, 1 error

Dafny is unable to prove the ensures foo(m); clause, even though the method cannot possibly modify anything. The problem seems to be that the OpaqueFunc is opaque, but it shouldn't matter what this function is; it can't possibly contain an object which is modified, since no objects are modified.

[parno]

I think it may be connected to the handling of allocated w.r.t. opaque functions. Some evidence is that if you run with /allocated:2 (instead of the default of 3), then the file verifies. With the default, the framing axiom for foo says that the value of foo remains the same for heaps h0 and h1 if you can prove that forall non-null references o that are either m or in the set defined by OpaqueFunc(m), then h0[o] == h1[o]. However, the frame ensures for methodNotModifyingAnything says that forall non-null references that were allocated in h0, the heap reads are the same. So that isn't quite sufficient to prove the frame axiom for foo. When you run with /allocated:2, the frame axiom for foo changes to say that you only need to prove equivalent reads for non-null, allocated references, which then directly lines up with the ensures from methodNotModifyingAnything. Conversely, in /allocated:3, you can also add requires forall o :: o in OpaqueFunc(m) ==> allocated(o); to method f, and that also makes it go through.