[clang] [analyzer] Indicate UnarySymExpr is not supported by Z3 (PR #108900)

[via cfe-commits]

vabridgers wrote:

> I'm okay with the PR, but this leaves me wonder how did you end up with this crash? How did you manage to avoid all the zillion other ways to crash the Z3 solver? Have you experienced such issues?

Thanks Balazs, TBH I'm not sure we've found all the ways to crash the Z3 solver since we stopped random testing with Z3 when we came across this issue. But we're getting that restarted to see what else we find (with this workaround in place). We have seen Z3 crashes specific to our internal proprietary target and have merged upstream and downstream only changes for those cases. As I think you may recall, we have our own specialized fuzzing tool for our downstream changes, so occasionally we find things not found anywhere else. 

Do you know if there's any other random testing done for csa without and with Z3? 

Thanks

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