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

[Balazs Benics 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 "
----------------
steakhal wrote:

I considered this. But then the semantic would be unclear if they set the value 0 for it yet they "enable" Z3 refutation. It would be confusing to see that all reports are discarded (because none of them are "SAT" or "accepted") yet they enabled Z3 refutation.
I find that configuration combination, or even the value zero for this option a trap.

To resolve this, I could see 2 options:
1) Drop the `crosscheck-with-z3` and just use this `crosscheck-with-z3-attempts-on-timeout` to imply if Z3 crosscheck should be enabled or not.
2) Keep the current what I propose in this patch. (My preference)

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