Unroll first and last iteration in encoding

[JonasAlaif]

We should probably introduce a flag to enable this behaviour. I wasn't able to easily implement this as a Viper to Viper transformation since unrolling the last loop iteration there isn't trivial: ideally the while isn't transformed away to let Carbon do the hard work of e.g. finding which local vars to havoc etc. but then the body must be repeated after the while (unfolding the last loop iter, but Viper is unhappy since a local var might be redefined) and the loop condition must be changed to allow the last loop unrolling to be inserted.

Also, why does the current Carbon encoding first Assume(guard.not) and only then inhale(invs). It doesn't actually matter, but looks strage to assume facts about a heap location and only then inhale the permissions for it.