Incorrect C# compilation of discriminators with underscores

[jaylorch]

If a discriminator has an underscore in it, Dafny generates invalid C# code. The method name will have that underscore replaced with two underscores, but any call to that method will have the underscore unchanged. This problem doesn't exist in Dafny release 3.2.0, but does exist in 3.3.0 and in the current version.

One can reproduce this and get the following error:

(1876,15): error CS1061: 'D' does not contain a definition for 'is_D_1' and no accessible extension method 'is_D_1' accepting a first argument of type 'D' could be found (are you missing a using directive or an assembly reference?)

by running Dafny on a file with the following contents:

module M {
  datatype D = D_1(i: int) | D_2(b: bool)

  method DoIt (d: D)
  {
    if (d.D_1?) {
      print d.i;
    }
    else {
      print d.b;
    }
  }
}

Running Dafny with /spillTargetCode:3 further illuminates the issue. One can see that the method is defined as:

    public bool is_D__1 { get { return this is D_D__1; } }

but the call to that method is:

      if ((d).is_D_1) {