Filter & Sort Counterexamples by Binders

[rcosta358]

Description

This PR replaces the expression-based counterexample assignment filtering with VC-based that filters assignments using VC binders and sorts them by binder order.

Before

Found:
∀y. true
∀z. true
∀w¹⁷⁶. y <= w¹⁷⁶ && w¹⁷⁶ <= z

Counterexample:
z == 0
y == 0
w¹⁷⁶ == 0

After

Found:
∀y. true
∀z. true
∀w¹⁷⁶. y <= w¹⁷⁶ && w¹⁷⁶ <= z

Counterexample:
y == 0
z == 0
w¹⁷⁶ == 0

Type of change

• Bug fix
• New feature
• Documentation update
• Code refactoring

Checklist

• Added/updated tests under liquidjava-example/src/main/java/testSuite/ (Correct* / Error*)
• mvn test passes locally
• Updated docs/README if behavior or API changed

[CatarinaGamboa]

Can you add some before/after examples to the summary? To explain why the change

[rcosta358]

This is needed mainly to sort the counterexamples by binders, so they appear in the same order the binders appear in the error message. When there are multiple binders, the counterexamples appearing in the same order is nice for readability.

It also simplifies the code quite a bit. However, with this change enum constants and static final constants no longer appear in the counterexample, which we discussed offline. For that I think we can have a separate simplification just for the expected type to be able to simplify aliases, enums, and static final constants.

[rcosta358]

Also added the before/after example.