We allow to reuse symbolic dereference objects to increase precision of the verification. One of the conditions for the reuse is that the dereferenced pointer must not have been overridden from the point of the last symbolic deref definition.
This condition contains a bug, though, as it assumed that the last definition is always an assignment. With unwinding in place, it can also be a phi instruction, so this commit adds that possibility.
We allow to reuse symbolic dereference objects to increase precision of the verification. One of the conditions for the reuse is that the dereferenced pointer must not have been overridden from the point of the last symbolic deref definition.
This condition contains a bug, though, as it assumed that the last definition is always an assignment. With unwinding in place, it can also be a phi instruction, so this commit adds that possibility.
Contains also a reproducer regression test.