[clang] [llvm] [analyzer][NFC] Reorganize Z3 report refutation (PR #95128)

[Balazs Benics via cfe-commits]

steakhal wrote:

Thanks for the review!

> LGTM. I didn't deeply analyze all the small details of the commit, but it is clearly NFC (builds better infrastructure for follow-up commits), the implementation is clear and elegant (slightly better quality than what I can write) and the tests demonstrate that it's working.

The problem is that currently one can't run tests with Z3 crosschecking. Consequently, no tests cover this functionality.
The unit-tests in the next PR tests the Z3 oracle, which is not tight to the actual Z3 library in an ways.

> IMO feel free to merge this and continue with the next commit.

Please have a second look at the llvm-related changes. Z3 has a really dangerous C API. I shot myself in the foot literally 3 times while working on this PR.

And btw notice that I removed the `proof=false` configuration as that is the default AFAIK, so that's why that is missing.

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