steakhal 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? https://github.com/llvm/llvm-project/pull/108900