Flatten Variable Derivation Chains

[rcosta358]

This PR improves the simplification for expressions by flattening variable derivation chains to avoid redundancy.
When a variable's origin is the same variable instance (e.g., #y_3 => #y_2), we collapse the chain to use the final node directly, eliminating redundant nested VarDerivationNodes in the derivation tree.

Example

#x_4 == (-#y_3) * (2) && #y_3 == #y_2 && #y_2 == 3

Before

...
{
    "value": 3,
    "origin": {
        "var": "#y_3",
        "origin": {
            "var": "#y_2"
        }
    }
}
...

After

...
{
    "value": 3,
    "origin": {
        "var": "#y_2"
    }
}
...

[CatarinaGamboa]

So the example would look like:
#x_4 == (-#y_2) * (2) && #y_2 == 3
right?

[CatarinaGamboa]

I'm just not super sure about this because it will have more disconnect from code right?
Lets say we have:
#x_4 == (-#z_3) * (2) && #z_3 == #y_2 && #y_2 == 3

That expression probably came from code like:

int y = 3;
int z = y;
@Refinement(...)
int x = -z *2;

If we are say that #x == (-#y) * (2) && #y_2 == 3 it can leave the user wondering why is x==y and we said it was x==z. It creates more disconnect between the error message and the code.

Now, if you are mentioning flattening variable instances for the same variable like y_1 and y_2, that makes more sense, since they are only internal representations but if we have a connection through a different variable, I'm not sure we should flatten it

[rcosta358]

You're right. Let me try only flattening variable instances for the same variable.

[alcides]

I think Catarina raises an interesting point, but with tens of variables, I'm not sure I would want to play "connect the dots" with all variables.

In some cases, I want it all collapsed (to see that I am accessing out of bounds), and in other cases I would want (as Catarina) the connection to the variables in the code first and front.

We might need to write some more real-world examples to decide the best default behavior, but in principle, I like that we are able to simplify as most as possible, but then expand to connect to the source code.

[CatarinaGamboa]

Yeah maybe with very large programs it becomes useful, but for debugging it will be a pain to understand where each predicate is created. I think most examples we have are rather small but we can try creating some bigger ones to test it on