Bad encoding for `this` in tail recursive functions when compiling to Java

[fabiomadge]

Dafny version

master

Code to produce this issue

class C {
  var data: nat
  constructor() {}
  function Loop(xs: seq<()>): () reads this {
    if |xs| == 0
    then ()
    else
      var _ := forall c :: c in { this } ==> c.data == this.data;
      var _ := set n: nat {:trigger n * 1} | n < 100 && n == this.data;
      var _ := map n: nat {:trigger n * 1} | n < 100 :: this;
      Loop(xs[1..])
  }
}

method Main(){
  var c := new C();
  print c.Loop([(), ()]), "\n";
}

Command to run and resulting output

No response

What happened?

Java lambdas don't support the way we use them.

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

Mac

[stefan-aws]

Can confirm that running above code with java as target throws an error (error: local variables referenced from a lambda expression must be final or effectively final).