Disjunctive pattern matching not correctly handled

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

datatype D = A(int) | C(int) {
  function Test(): D {
    match this{
      case A(_) | C(_) =>
        this
    }
  }
}
method Main() {
  print C(0).Test();
}

Command to run and resulting output

dafny run -t:cs file.dfy

What happened?

Dafny program verifier finished with 0 verified, 0 errors
Unhandled exception. System.InvalidCastException: Unable to cast object of type '_module.D_C' to type '
_module.D_A'.
   at _module.D.get_dtor_A_a0()
   at _module.D.Test()
   at _module.__default._Main(ISequence`1 __noArgsParameter)
   at __CallToMain.<>c__DisplayClass0_0.<Main>b__0()
   at Dafny.Helpers.WithHaltHandling(Action action)
   at __CallToMain.Main(String[] args)

The translation is the following:

      bool unmatched0 = true;
      if (unmatched0) {
        bool disjunctiveMatch0 = false;
        BigInteger _0___v2 = _source0.dtor_A_a0;
        disjunctiveMatch0 = true;
        BigInteger _1___v3 = _source0.dtor_C_a0;
        disjunctiveMatch0 = true;
        if (disjunctiveMatch0) {
          unmatched0 = false;
          return this;
        }
      }

Since disjunctive patterns may not bind variables, we should simply not translate the patterns "_" into variable extraction.

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

Windows