The var_eq analysis does not check if variables might be written by multiple threads.
It is possible to construct a case, where a pointer to one variable (e.g. z) is passed to multiple threads. Within one of the threads, the equality between this z and another variable is tracked, even though the other thread might change the variable z, invalidating the equality relation.
An example of this issue can be found here.
related issue: #743