Anomaly in ecSubst when postconditions contain Pr[...] expressions

[fdupress]

The following illustrates one such failure. Aaron (github handle?) has one that fails on wp but has a much larger context that I cannot usefully reduce.

This can still be worked around using pose, so not blocking, but certainly annoying.

require import AllCore Distr DBool.

module M = {
  proc p() = {
    var b;

    b <$ dbool;
    return b;
  }
}.

lemma ohno &m:
  Pr[M.p() @ &m: res] = Pr[M.p() @ &m: !res].
proof.
byphoare=> //.
proc; rnd. conseq />.

Fails with anomaly: File "src/ecCoreSubst.ml", line 149, characters 2-8: Assertion failed