Another case where why3 isn't really in the place that one wants, is when one has an invariant in a function that is larger than what one can see on the screen. It seems that for invariants, why3 always considers the name of the function to be relevant (orange), whereas I would rather see the invariant that I am working on.