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

Reply via email to