fix issue #11: encode may analyses properly.
We can encode may analyses at SMT level by introducing a new variable that can be either true or false if the result holds, effectively encoding imprecisions of analyses