<div dir="ltr">There are multiple problems with the relevant code:<br><a href="https://github.com/llvm/llvm-project/blob/master/clang/test/Analysis/analyzer_test.py#L18-L29">clang/test/Analysis/analyzer_test.py</a><br><span style="font-family:monospace">```<br>if 'z3' not in test.requires:<br>    results.append(self.executeWithAnalyzeSubstitution(<br>        saved_test, litConfig, '-analyzer-constraints=range'))<br><br>    if results[-1].code == lit.Test.FAIL:<br>        return results[-1]<br><br># If z3 backend available, add an additional run line for it<br>if self.use_z3_solver == '1':<br>    assert(test.config.clang_staticanalyzer_z3 == '1')<br>    results.append(self.executeWithAnalyzeSubstitution(<br>        saved_test, litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3'))<br>```</span><br><br>1) If you watch closely, tests that 'REQUIRES: z3' won't run unless you specify the undocumented USE_Z3_SOLVER=1 llvm-lit parameter.<br>So even if I have z3 installed, the corresponding test would still not run - which is somewhat counter-intuitive.<br><br>2) Even if you additionally specify the magic flag, your tests would run, except with the z3 based constraint manager (z3-CM) - so strictly speaking - not your test configuration would run.<br>This is problematic if your test depends on the simplified (flawed) behavior of the range-CM in certain situations.<br><br>3) If the test file does not require z3 but the USE_Z3_SOLVER is enabled.<br>First, the test file would be checked using the range-CM, and (assuming it passed) checked again using the z3-CM.<br>There is some chance, that on a given test file, that the generated exploded graph will be significantly different.<br>Due to these differences, we should not assume that the bugreports that are expected in the test file would match with the actual reports in both cases.<br>This is especially problematic since this additional run was added by the test suite rather than the test author.<br><br><br>Conclusion:<br>'REQUIRES: z3' should really mean whether you have clang built with z3 or not. (in other words, you have z3 installed or not)<br>We should have some way (eg. another keyword?) specifying that this test file can be run with z3-CM. (something like: ALSO_RUN_WITH_Z3_SOLVER)<br>In such files, all RUN commands should be executed normally, but also with the z3-CM if z3 is available.<br><br>Since the z3-CM is really slow, it is reasonable to have some way to skip such tests, but no more than necessary.<br>I assume, that USE_Z3_SOLVER tried to serve exactly this purpose.<br>Probably 'ALLOW_Z3_CONSTRAINT_MANAGER' would be a better name and we should have some sort of documentation about this parameter.<br><br>If the test file requires z3 and contains run commands using only the z3-CM, then that test should be categorized as UNSUPPORTED if ALLOW_Z3_CONSTRAINT_MANAGER was not enabled.<br>Tests that require z3 but only for crosscheck, should run regardless of the ALLOW_Z3_CONSTRAINT_MANAGER param.<br><br><br>By the same token, do we even have build bots using this USE_Z3_SOLVER lit param?<br>Or even having z3 installed?<br><br>What are your thoughts about this?<br>Is this approach reasonable to you?<br><br><br>Let me know if I missed something.<br><br>Regards, Balazs<br></div>