================
@@ -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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
