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

[Donát Nagy via cfe-commits]

================
@@ -213,6 +215,15 @@ ANALYZER_OPTION(
     "400'000 should on average make Z3 queries run for up to 100ms on modern "
     "hardware. Set 0 for unlimited.", 0)
 
+ANALYZER_OPTION(
+    unsigned, Z3CrosscheckRetriesOnTimeout,
+    "crosscheck-with-z3-retries-on-timeout",
+    "Set how many times the oracle is allowed to retry a Z3 query. "
+    "Set 0 for not allowing retries, in which case each Z3 query would be "
+    "attempted only once. Increasing the number of retries is often more "
----------------
NagyDonat wrote:

`<bikeshedding>`
I think it would be more natural to introduce an option called `"crosscheck-with-z3-attempts-on-timeout"` which includes the initial attempt. (When I first read the patch, I didn't notice that you're only counting the REtries and you need to add one to this option to get the real number of attempts. I fear that this could surprise other readers as well.)
`</bikeshedding>`

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