Fix: Removed wrong "related position" precision when dealing with regrouped quantifiers

[MikaelMayer]

This PR fixes #2211
After investigation it looks like the following expression

forall i | 0 <= i < |s| :: // Normal token
    && P1(s[i])
    && P2(s[i])

was split in two while searching for triggers

forall i | 0 <= i < |s| :: // Nested token, outer pointing to "forall", inner pointing to "P1"
    P1(s[i])
forall i | 0 <= i < |s| :: // Nested token, outer pointing to "forall", inner pointing to "P2"
    P2(s[i])

But another pass for searching for triggers regroups quantifiers which have the same bound variables and same triggers. Since the two expressions have the same trigger s[i], they are regroupped with an AND back to:

forall i | 0 <= i < |s| :: // Nested token, outer pointing to "forall", inner pointing to "P1"
    P1(s[i]) && P2(s[i])

As you can see, the problem of the regrouping is that it takes the token of the first element of the group, which had an indication that it pointed to P1.
The last related location of #2211 thus was an artefact of the token being copied without paying attention to that detail. Since we regroup the tokens, there is no nested token there to have so this PR removes nested tokens when regrouping comprehensions to avoid giving false information.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[RustanLeino]

Thanks for the good description. From that description, this fix looks good.

Can you add another test that will exercise the is ExistsExpr branch of the code as well?

[MikaelMayer]

Thanks for the good description. From that description, this fix looks good.

Can you add another test that will exercise the is ExistsExpr branch of the code as well?

I added a test and verified that the output was different before this PR, it included the unwanted error location.