Fix Self-Referential Assignments

[rcosta358]

This PR fixes #176, where a simple assignment x = x + 1 would cause a false negative in the verification.

Root Cause

In the joinPredicates method, creating a new VCImplication with Variable.getRefinement() added the constraint x == lastInstance to connect the variable with its current value. However, when the assignment is self-referential (e.g., x = x + 1), it introduced a contradictory cycle in the SMT premises. Then, Z3 couldn't find a counterexample, therefore concluding the verification was correct.

Solution

Added two helper methods to detect and prevent these cycles:

• hasDependencyCycle: checks if the value of a variable references itself transitively
• hasVariable: checks if a variable is present in a given expression

Then, when a cycle is detected, we use getMainRefinement() instead of getRefinement().

[alcides]

An alternative solution would be to have a proper VC representation:

\forall x:int, pred -> another_vc | final_cond. This could just be a list of predicates, where the last one is the conclusion. But the ordering of the binders allows to know exactly what you can and cannot do.

For instance, you cannot replace inner bindings in outside expressions, but the other way you can.