[clang] [analyzer][Z3] Restore the original timeout of 15s (PR #118291)

Balazs Benics via cfe-commits cfe-commits at lists.llvm.org
Tue Dec 3 06:45:50 PST 2024


================
@@ -189,20 +189,23 @@ ANALYZER_OPTION(
     "crosscheck-with-z3-eqclass-timeout-threshold",
     "Set a timeout for bug report equivalence classes in milliseconds. "
     "If we exhaust this threshold, we will drop the bug report eqclass "
-    "instead of doing more Z3 queries. Set 0 for no timeout.", 700)
+    "instead of doing more Z3 queries. On fast machines, 700 is a sane value. "
+    "Set 0 for no timeout.", 0)
 
 ANALYZER_OPTION(
     unsigned, Z3CrosscheckTimeoutThreshold,
     "crosscheck-with-z3-timeout-threshold",
-    "Set a timeout for individual Z3 queries in milliseconds. "
-    "Set 0 for no timeout.", 300)
+    "Set a timeout for individual Z3 queries in milliseconds. On fast "
+    "machines, 400 is a sane value. "
+    "Set 0 for no timeout.", 15'000)
 
 ANALYZER_OPTION(
     unsigned, Z3CrosscheckRLimitThreshold,
     "crosscheck-with-z3-rlimit-threshold",
-    "Set the Z3 resource limit threshold. This sets a deterministic cutoff "
-    "point for Z3 queries, as longer queries usually consume more resources. "
-    "Set 0 for unlimited.", 400'000)
+    "Set the Z3 resource limit threshold. This sets a supposedly deterministic "
+    "cutoff point for Z3 queries, as longer queries usually consume more "
+    "resources. "
+    "Set 0 for unlimited.", 0)
----------------
steakhal wrote:

```suggestion
    "Set the Z3 resource limit threshold. This sets a supposedly deterministic "
    "cutoff point for Z3 queries, as longer queries usually consume more "
    "resources. "
    "400'000 should on average make Z3 queries run for up to 100ms on modern hardware."
    "Set 0 for unlimited.", 0)
```

Could you please confirm that we need to set this option to zero to not have flaky reports?

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


More information about the cfe-commits mailing list