Imprecise refinement in Value Checker in loops

Consider the following loop:

    void test() {
        for (int i = 0; i < 12; i++) {
            @IntRange(from = 0, to = 12) int j = i;
        }
    }

I would expect this code to typecheck. Instead, the following error is issued:

error: [assignment.type.incompatible] incompatible types in assignment.
            @IntRange(from = 0, to = 12) int j = i;
                                                 ^
  found   : @IntRange(from=0, to=127) int
  required: @IntRange(from=0, to=12) int
1 error

This is very strange behavior - I don't know why the Value Checker might think that 0 to 12 -> 0 to 127.

Start by reproducing the Java loop in the Value Checker and trace how its loop refinement derives the reported 0-to-127 range. Compare that result with the expected 0-to-12 range; done means the snippet typechecks and the regression is covered by an appropriate test.