[clang] [analyzer] Correct crash in Z3 wrapper (PR #158276)

[via cfe-commits]

vabridgers wrote:

> The tests look really fragile. Without knowing exactly how did we end up with a SymExpr that fails to convert to a Z3 formula, I'm tempted to push back. I think I've seen similar conversion errors and fixes from you. This suggests to me that we need to understand the underlying reasons why we have these SymExprs and systematically solve these issues.
> 
> My gut instincts suggests that this SymExpr lacks some SymbolCast (due to the inappropriate modeling of casts), which bites back here as well. If that's the case, we could provide a translation layer that would visit a SymExpr and output a valid SymExpr that has the bit-widening/truncating SymbolCasts where needed. That way only Z3 would have a different "view" of these symbols while the engine could still have the wrong SymExprs. The added benefit would be to have a centralized place of the hacks that we currently embed into the Z3 expr converter.

Hi @steakhal , thanks for the comment. I agree there could be some deeper issue here, but my immediate concern is to avoid the crash. Is it ok if we separate those concerns and first come up with a way to avoid the crash, then follow up with understanding and fixing the deeper concern? I admit I do not understand the details of SymExprs, but I needed to get attention on this new issue - hence this PR as a starting point. 

https://github.com/llvm/llvm-project/pull/158276