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

DonĂ¡t Nagy via cfe-commits cfe-commits at lists.llvm.org
Mon Dec 2 08:14:18 PST 2024


https://github.com/NagyDonat approved this pull request.

The commit which introduced the new Z3 timeout logic (https://github.com/llvm/llvm-project/pull/97298) was landed with my approval, but since then I realized that this was a mistake -- in particular the concrete fine-tuned default values provide a good fit for one particular computer speed and (as the experimental results show) behave badly on systems that are significantly slower than that. (This should have been obvious in hindsight, but I missed it.)

Based on this I support restoring the legacy 15 second timeout which is good as a sane default value and ensures that even the slow computers finish practically all non-hanging Z3 calculations.

Changing these `ANALYZER_OPTION`s might be useful for power users who can measure the speed of their worker nodes and configure some sharper timeouts that work for them in particular; but even that is a questionable decision, because with sharp timeouts a temporary loss of processing power (e.g. a job that's started in parallel on the same machine) can cause inconsistent results. 

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


More information about the cfe-commits mailing list