If you have a loop whose invariant takes in more and more of a sequence with each iteration, DafnyCC will typically need you to explicitly assert the relationship between the old sequence and the new sequence. For instance:
while j < |a|
invariant a[..j] == b[..j];
a[j] := b[j];
assert a[..j+1] == a[..j] + [a[j]]; // this line added for DafnyCC's sake
assert b[..j+1] == b[..j] + [b[j]]; // this line added for DafnyCC's sake
j := j + 1;
This also applies to sequences derived from arrays. For instance, in the example above, the reminders above are necessary whether a and b are sequences or arrays.