Does this loop invariant guarantee that the variable never changes?
The loop invariant doesn't "guarantee" anything. It is a summary of relevant information you know about the state of the program when it reaches that point. If your loop is e.g.:

k = 5;
...
for(int i = 0; i &lt; N; i++) {
   /* Invariant: k = 5 */
   ...
   k = 207;
   ...
   frob_very_hard(&amp;k);
   ...
   k *= 3;
   ...
   k = 5;
}


at the marked point k == 5, but not all over the program.