Java Compilation Crash: Datatype Update inside For Loop

[alex-usher]

trafficstars

Dafny version

4.1.0

Code to produce this issue

datatype D0 = DC1(cf1: int, cf2: int)

method Main() {
    for i := 1 to 2 {
        print DC1(1, 2).(cf1 := i);
    }
}

Command to run and resulting output

$ dafny main.dfy /compileTarget:java

Dafny program verifier finished with 1 verified, 0 errors
Wrote textual form of target program to main-java/main.java
....
main-java/_System/__default.java:18: error: local variables referenced from a lambda expression must be final or effectively final
          return ((D0)(java.lang.Object)(dafny.Helpers.<java.math.BigInteger, D0>Let(_0_i, boxed2 -> {
                                                                                     ^
1 error
Error while compiling Java files. Process exited with exit code 1

What happened?

Compiling the above program into Java verifies successfully but throws the above exception when compiling the jar. All other backends compile successfully. I've seen this error message in other test cases (#3910), but this seems to be related to a different language feature so I'm listing this as a new issue. I believe the error is specifically related to using i (changing i to other values/variables removes the issue). Thanks!

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

Linux, Mac