Reassignment of a variable using a previous value of that variable results in false path condition terms

[hgouni]

Reassignment of a variable to itself, with an additional modification to the right hand side of the assignment, results in false path condition terms. This causes, for example, check to always return true, because for all x, false => x. As a concrete example, the statement x.g := x.g + 1 may result in a path condition like x.g == x.g + 1. This path condition is false; it should use a reference to the old value of x.g on the right hand side. The symbolic execution rules and implementation should be updated to address this.

[jennalwise]

There was a flaw in the design of the exec rule for field assignment. I have since fixed the design flaw in the documentation and am in the process of implementing the fix in the code.

[jennalwise]

Code fix implemented in this commit: https://github.com/gradual-verification/silicon-gv/commit/bba7e79d070493e1d3118401e5f5b32a860d84c3