[clang] [analyzer] Retry UNDEF Z3 queries 2 times by default (PR #120239)

DonĂ¡t Nagy via cfe-commits cfe-commits at lists.llvm.org
Mon Jan 6 08:23:56 PST 2025


================
@@ -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:

By the way, if I don't _resolve_ something in github, I probably just forgot to do it. I know about this feature and I try to use it when I remember (because I agree that it's a good utility), but it's not (yet) an automatic reflex that I always perform when I should. If a thread is left unresolved, feel free to ask me about it, or if my other comment suggest that I'm accepting the commit, then just ignore it. 

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


More information about the cfe-commits mailing list