improve handling of undef behavior in store instructions
After executing undef behavior, a store may or may not happen. Thus, reflect
this possiblity in the SMT encoding using quantified boolean vars