Compilation Error: generates duplicate local variable declarations

[laurejt]

Dafny verifies the following program, but generates invalid code.

datatype bar = Bar
datatype obj = Obj(fooBar:map<foo,bar>)
datatype foo = Foo

method test_case() returns (o:obj)
{
    if true {
        o:= o.(fooBar := o.fooBar[Foo := Bar]);
    }
}

The compilation error generated is:

error CS0136: A local variable named '_pat_let_tv1' cannot be declared in this scope because it would give a different meaning to '_pat_let_tv1', which is already used in a 'parent or current' scope to denote something else

The segment of the generated code causing this error is:

public static void @test__case(out @obj @o)
  {
    @o = new @obj();
  TAIL_CALL_START: ;
    var @_pat_let_tv1= @o;
    if (true)
    {
      var @_pat_let_tv1= @o;
      @o = Dafny.Helpers.Let<@obj,@obj>(@o, _pat_let0_0 => Dafny.Helpers.Let<@obj,@obj>(_pat_let0_0, @_2_dt__update__tmp_h0 => new @obj(new obj_Obj(((@_pat_let_tv1).@dtor_fooBar).Update(new @foo(new foo_Foo()), new @bar(new bar_Bar()))))));
    }
  }

If the if statement is removed, code generation is correct.