Improve Counterexamples

[rcosta358]

This PR improves the counterexamples by filtering out assignments that are already present in the context, since these don't add any new information to the verification state.

Examples

---

Before

After

---

Before

After

[CatarinaGamboa]

I'm not sure I get what the goal is here. Its because we are already showing the most simplified version in the refinement error that we don't need the other values?

I'm especially confused about the 2nd example, its very weird that we show #a_2 == X and not #a_1. Should we also be removing #a_2 since it is nowhere in the simplified error message?

Also, it raises a question, should we just present the simplified error version in the console version? in the ide we can expand it but here could be helpful to also present the full-on error message to match the counterexample.

(unrelated but these errors will be much better when we apply #162 )

[CatarinaGamboa]

need to understand the objective better ^^

[rcosta358]

This is not really about filtering out assignments that are not present in the simplified expression of the error message, but about filtering out the assignments that are already present in the context. This change resulted from a conversation with @alcides, where we agreed that if the context already includes a refinement shown in the counterexample, we consider it redundant and remove it to simplify the counterexample.

[rcosta358]

Regarding showing unsimplified expressions in the command-line version, maybe we could add a command argument like --no-simplification to do so, but I think always showing both versions would be too verbose.

[alcides]

The main point is:

void f(@Refined("x > 0") int x) {
   int a = 3;
   f(x - a);
}

In this case, the counter example showing that a == 3 is not very useful, because it was assigned before (there may be thousands of variables in the body, including those from anf). We care about the x, because its refinement is not an equality, so a proper witness matters.

Does this make sense? or am I missing some other case, where showing other variables (we know about) is relevant?