False positive from side-effect check in loop contracts

[SaswatPadhi]

CBMC version: develop
Operating system: Mac OS 10.15

Running --enforce-all-contracts raises a false positive on the following file:

int main()
{
  int i, N, *a = malloc(sizeof(int));

  for(i = *a; i < N; ++i)
    __CPROVER_loop_invariant(
      (*a > N) ||
      (*a <= i && i <= N)
    )
  {
    ++i;
  }
}

Exact command line:

$ goto-cc test.c -o 1.gb
$ goto-instrument --enforce-all-contracts 1.gb 2.gb
--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-programs/goto_convert.cpp:877 function: convert_loop_invariant
Condition: loop invariant is not side-effect free
Reason: no_sideeffects.instructions.empty()
Backtrace:
...

What behaviour did you expect:
goto-instrument shouldn't reject this file. The invariant seems free of side effects -- it only performs basic arithmetic comparisons and read-only heap access.