Problematic Path-condition Solving.

[DesNevermore]

I noticed in the path condition solving module in saber implementation, it will create a brand new Z3 variable based on the instruction of the path condition. This can lead to inaccuracy to the solving result. Say we have a code snippet as below:

So, when I use saber to do the path-condition solving, it will create 3 different Z3 variables for the three condition:

And it is easy to know the result has to be SAT:

I am not sure whether this is designed to be this or a mistake?