@@ -189,14 +189,19 @@ ANALYZER_OPTION(
189189 " crosscheck-with-z3-eqclass-timeout-threshold" ,
190190 " Set a timeout for bug report equivalence classes in milliseconds. "
191191 " If we exhaust this threshold, we will drop the bug report eqclass "
192- " instead of doing more Z3 queries. On fast machines, 700 is a sane value. "
192+ " instead of doing more Z3 queries. Setting this to 700 ms in conjunction "
193+ " with \" crosscheck-with-z3-timeout-threshold\" of 300 ms, would nicely "
194+ " guarantee that no bug report equivalence class can take longer than "
195+ " 1 second, effectively mitigating Z3 hangs during refutation. "
193196 " Set 0 for no timeout." , 0 )
194197
195198ANALYZER_OPTION(
196199 unsigned , Z3CrosscheckTimeoutThreshold,
197200 " crosscheck-with-z3-timeout-threshold" ,
198- " Set a timeout for individual Z3 queries in milliseconds. On fast "
199- " machines, 400 is a sane value. "
201+ " Set a timeout for individual Z3 queries in milliseconds. "
202+ " On fast machines, 300 worked well in some cases. "
203+ " The lower it is, the higher the chances of having flaky issues. "
204+ " Having no timeout may hang the analyzer indefinitely. "
200205 " Set 0 for no timeout." , 15'000 )
201206
202207ANALYZER_OPTION(
@@ -205,7 +210,8 @@ ANALYZER_OPTION(
205210 " Set the Z3 resource limit threshold. This sets a supposedly deterministic "
206211 " cutoff point for Z3 queries, as longer queries usually consume more "
207212 " resources. "
208- " Set 0 for unlimited." , 0 )
213+ " 400'000 should on average make Z3 queries run for up to 100ms on modern "
214+ " hardware. Set 0 for unlimited." , 0 )
209215
210216ANALYZER_OPTION(bool , ShouldReportIssuesInMainSourceFile,
211217 " report-in-main-source-file" ,
0 commit comments