Fix Z3 refutation detection
Z3 refutation availability is checked by reading the help page of
Clang analzer options. However, it is possible that the analyzer
option exists, but Clang itself is not compiled with Z3. So we
consider Clang Z3 refutation capable if it was also compiled with
Z3.
Fixes
@@ -72,6 +72,13 @@ def is_z3_capable(context):
def is_z3_refutation_capable(context):
""" Detects if the current clang is Z3 refutation compatible. """
+
+ # This function basically checks whether the corresponding analyzer config
+ # option exists i.e. it is visible on analyzer config option help page.
+ # However, it doesn't mean that Clang itself is compiled with Z3.
+ if not is_z3_capable(context):
+ return False
+
check_supported_analyzers([ClangSA.ANALYZER_NAME], context)
analyzer_binary = context.analyzer_binaries.get(ClangSA.ANALYZER_NAME)
