[clang] 43082d6 - [analyzer] Rename z3 constraint manager backend to unsupported-z3 (#205370)

[via cfe-commits]

Author: Balázs Benics
Date: 2026-07-02T12:31:30Z
New Revision: 43082d6efa9c819a7b4ddf4ecfa963748caa82de

URL: https://github.com/llvm/llvm-project/commit/43082d6efa9c819a7b4ddf4ecfa963748caa82de
DIFF: https://github.com/llvm/llvm-project/commit/43082d6efa9c819a7b4ddf4ecfa963748caa82de.diff

LOG: [analyzer] Rename z3 constraint manager backend to unsupported-z3 (#205370)

The Z3 constraint manager backend (selected via
-analyzer-constraints=z3) is unmaintained and known to crash on
real-world input. Rename the user-facing flag to unsupported-z3 and
reword its description so users see up front that the backend is
unsupported and crash-prone -- patches welcome, crash reports are not.

Assisted-By: claude

Added: 
    

Modified: 
    clang/docs/ReleaseNotes.md
    clang/include/clang/Basic/DiagnosticDriverKinds.td
    clang/include/clang/StaticAnalyzer/Core/Analyses.def
    clang/test/Analysis/missing-z3-nocrash.c
    clang/test/Analysis/z3/D83660.c
    clang/test/Analysis/z3/pretty-dump.c
    clang/test/Analysis/z3/z3-unarysymexpr.c

Removed: 
    


################################################################################
diff  --git a/clang/docs/ReleaseNotes.md b/clang/docs/ReleaseNotes.md
index fc8b0d369b979..0f252fdf3601b 100644
--- a/clang/docs/ReleaseNotes.md
+++ b/clang/docs/ReleaseNotes.md
@@ -1057,6 +1057,10 @@ latest release, please see the [Clang Web Site](https://clang.llvm.org) or the
 
 ### Static Analyzer
 
+- The `-analyzer-constraints` option `z3` was renamed to `unsupported-z3`
+  because the Z3-based (constraint) solver was known for crashing for years now.
+  Didn't receive support, so it was marked unsupported.
+
 #### Crash and bug fixes
 
 - Fixed `security.VAList` checker producing false positives when analyzing

diff  --git a/clang/include/clang/Basic/DiagnosticDriverKinds.td b/clang/include/clang/Basic/DiagnosticDriverKinds.td
index 8edac14f4972a..3f8fc16e346cf 100644
--- a/clang/include/clang/Basic/DiagnosticDriverKinds.td
+++ b/clang/include/clang/Basic/DiagnosticDriverKinds.td
@@ -597,8 +597,8 @@ def err_analyzer_checker_option_invalid_input : Error<
 def err_analyzer_checker_incompatible_analyzer_option : Error<
   "checker cannot be enabled with analyzer option '%0' == %1">;
 def err_analyzer_not_built_with_z3 : Error<
-  "analyzer constraint manager 'z3' is only available if LLVM was built with "
-  "-DLLVM_ENABLE_Z3_SOLVER=ON">;
+  "analyzer constraint manager 'unsupported-z3' is only available if LLVM was "
+  "built with -DLLVM_ENABLE_Z3_SOLVER=ON">;
 
 def warn_drv_needs_hvx : Warning<
   "%0 requires HVX, use -mhvx/-mhvx= to enable it">,

diff  --git a/clang/include/clang/StaticAnalyzer/Core/Analyses.def b/clang/include/clang/StaticAnalyzer/Core/Analyses.def
index 51803e7c1f0d2..8ef7f2e6c7d3f 100644
--- a/clang/include/clang/StaticAnalyzer/Core/Analyses.def
+++ b/clang/include/clang/StaticAnalyzer/Core/Analyses.def
@@ -18,7 +18,9 @@ ANALYSIS_CONSTRAINTS(RangeConstraints, "range",
                      "Use constraint tracking of concrete value ranges",
                      CreateRangeConstraintManager)
 
-ANALYSIS_CONSTRAINTS(Z3Constraints, "z3", "Use Z3 contraint solver",
+ANALYSIS_CONSTRAINTS(Z3Constraints, "unsupported-z3",
+                     "[UNSUPPORTED] Z3 SMT solver. Known to crash; patches "
+                     "welcome, crash reports are not.",
                      CreateZ3ConstraintManager)
 
 #ifndef ANALYSIS_DIAGNOSTICS

diff  --git a/clang/test/Analysis/missing-z3-nocrash.c b/clang/test/Analysis/missing-z3-nocrash.c
index 2e345ad00f5ab..ca2e4e038dc03 100644
--- a/clang/test/Analysis/missing-z3-nocrash.c
+++ b/clang/test/Analysis/missing-z3-nocrash.c
@@ -1,5 +1,5 @@
-// RUN: not %clang_analyze_cc1 -analyzer-constraints=z3 %s 2>&1 | FileCheck %s
+// RUN: not %clang_analyze_cc1 -analyzer-constraints=unsupported-z3 %s 2>&1 | FileCheck %s
 // UNSUPPORTED: z3
 
-// CHECK: error: analyzer constraint manager 'z3' is only available if LLVM
-// CHECK: was built with -DLLVM_ENABLE_Z3_SOLVER=ON
+// CHECK: error: analyzer constraint manager 'unsupported-z3' is only available
+// CHECK-SAME: if LLVM was built with -DLLVM_ENABLE_Z3_SOLVER=ON

diff  --git a/clang/test/Analysis/z3/D83660.c b/clang/test/Analysis/z3/D83660.c
index b4f0539f7e8a7..ad230de8a620d 100644
--- a/clang/test/Analysis/z3/D83660.c
+++ b/clang/test/Analysis/z3/D83660.c
@@ -1,6 +1,6 @@
 // RUN: env Z3_SOLVER_RESULTS="SAT,SAT,SAT,SAT,UNDEF" \
 // RUN: LD_PRELOAD="%llvmshlibdir/MockZ3SolverCheck%pluginext" \
-// RUN: %clang_analyze_cc1 -analyzer-constraints=z3 \
+// RUN: %clang_analyze_cc1 -analyzer-constraints=unsupported-z3 \
 // RUN:   -analyzer-checker=core %s -verify
 //
 // REQUIRES: z3, z3-mock, asserts, system-linux

diff  --git a/clang/test/Analysis/z3/pretty-dump.c b/clang/test/Analysis/z3/pretty-dump.c
index e6cd6d83373b8..a20004c0c335d 100644
--- a/clang/test/Analysis/z3/pretty-dump.c
+++ b/clang/test/Analysis/z3/pretty-dump.c
@@ -1,4 +1,4 @@
-// RUN: %clang_analyze_cc1 -analyzer-constraints=z3 \
+// RUN: %clang_analyze_cc1 -analyzer-constraints=unsupported-z3 \
 // RUN:   -analyzer-checker=core,debug.ExprInspection %s 2>&1 | FileCheck %s
 //
 // REQUIRES: z3

diff  --git a/clang/test/Analysis/z3/z3-unarysymexpr.c b/clang/test/Analysis/z3/z3-unarysymexpr.c
index efe558c3146e8..bcdc2b6a66f10 100644
--- a/clang/test/Analysis/z3/z3-unarysymexpr.c
+++ b/clang/test/Analysis/z3/z3-unarysymexpr.c
@@ -1,5 +1,5 @@
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s \
-// RUN:  -analyzer-constraints=z3
+// RUN:  -analyzer-constraints=unsupported-z3
 // RUN: %clang_analyze_cc1 -verify %s \
 // RUN:  -analyzer-checker=core,debug.ExprInspection \
 // RUN:  -analyzer-config crosscheck-with-z3=true