Reference Highlighting corresponding variable with position in source code

[SpringVaS]

When selecting variables in the sequent to be highlighted in the source, an inconsistency is observable.
a bound (e. g. by let) variable is sometimes not highlighted in at the same position in sequent (formula) and source.

The first image shows a highlighting selecetion of the variable s in the Term s < |this.seqq|. Yet, in the code the variable s is highlighted at the position of the condition s >= 0.

The second image (with undbound variables) shows the expected behaviour.

let:

no let:

[JonasKlamroth]

maybe im missing the point but to me all those highlightings seem to be correct. what would be the expected result in your opinion?