Rewriter did not respect order of annotations

[sakehl]

/*@
  requires ant1 != NULL && \pointer_length(ant1) == _n_vis;
  requires (\forall* int i; 0<=i && i< \pointer_length(ant1); Perm(&ant1[i], write));
  requires (\forall int _0; 0 <= _0 && _0 < _n_vis; 0 <= ant1[_0]);
  requires _n_vis == 230930;
@*/
int SubDirection(int *ant1, int _n_vis) {
}

This program does not verify, it gives the error:

[---------------------------------------------------------------------
    5    requires (\forall int _0; 0 <= _0 && _0 < _n_vis; 0 <= ant1[_0]);
       ---------------------------------------------------------------------]
    6    requires _n_vis == 230930;
    7  @*/
--------------------------------------
The offset to the pointer may be outside the bounds of the allocated memory area that the pointer is in. (https://utwente.nl/vercors#ptrBlock)

This is because in (I think quantifier rewrite step) _n_vis is replaced by 230930 on line 4. But this is not valid, since the information of _n_vis == 230930 is only available from line 5 and onward.

I'll investigate where this happens.