[clang] [analyzer] Retry UNDEF Z3 queries at most "crosscheck-with-z3-retries-on-timeout" times (PR #120239)

[Donát Nagy via cfe-commits]

NagyDonat wrote:

> I adjusted the first commit message to highlight my answer to these questions. I hope that's clear enough.

Ok, I'd say that this explanation is _good enough_ to claim that "this change may be helpful" -- which is sufficient to merge this change, because it's conservative, non-disruptive and close to being an NFC change. (The only cost is that it increases code complexity, which is a pity IMO, but isn't a high priority problem...)

I think it would be good to include this reasoning in the final commit message of the merged commit that will be eventually placed on the main branch (unless you're strongly opposed to this).
 
> > To check this question, it would be nice to have measurements that compare the total analysis time and flakiness [...]
> 
> I think we discussed this under the RFC, but I want to make sure you confirm this before I'd discard this point.

As I said on discourse, think that the measurements (that I know of) are too noisy:
> Due to this noise in the measurement results, I feel that these eight runs are not enough to definitely demonstrate the usefulness of the suggested patch (i.e. that multiple small queries are better than just one query with an appropriately longer timeout). (At least their trend points in the right direction, but this trend is weaker than the definitely-just-noise trend that lower timeouts reduce the flakiness…)

However, I understand if you don't want to do more measurements (and want to merge this based on your good intuitions + the knowledge that it doesn't cause problems), then I'm not opposed and ready to accept this PR.

> @NagyDonat I think I'm ready for the next round of review.

Thanks for the updates! My only remaining open question is the bikeshedding about the name of the option, where I explained my position in an inline comment.

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