Remove irrelevant assignments from counterexamples

[palinatolmach]

We generate assignments for some globaly accessible variables, such as ORIGIN_ID and CALLER_ID, by default. To make the counterexample easier to interpret, we can restrict the model to the variables showing up in constraints.

[palinatolmach]

As pointed out by @PetarMax, we generate assignments to CALLER_ID and ORIGIN_ID, because they appear in path conditions (we have checks on them not being precompile addresses, Vm, Test contracts, etc). We could do post-processing on the model and exclude their assignments from the model manually, but there might be other constraints on their values if, e.g., access control checks are involved.

I think we can close it for now, and instead improve the counterexample presentation by translating variable names back to the Solidity representation (VV1_x_... to x) and CALLER_ID to msg.sender, so it's more clear.

[palinatolmach]

Reopened after a discussion with @ehildenb.

Another way to filter our non-informative CALLER_ID and SENDER_ID assignments is to check whether the constraints on these variables all appear in the initial term (or come from the ensures clause of a cheatcode such as freshAddress()), as a post-processing step.