Add release notes for r299463.

Implement z3-based constraint solver backend for clang static analyzer.

git-svn-id: https://llvm.org/svn/llvm-project/cfe/branches/release_50@311213 91177308-0d34-0410-b5e6-96231b3b80d8

diff --git a/docs/ReleaseNotes.rst b/docs/ReleaseNotes.rst
index d6bc7d18f13d1812363b3bc58adbb8a0ae7d784c..a5d459d333cfa3ba4c952565d594b8839a272cc2 100644 (file)
--- a/docs/ReleaseNotes.rst
+++ b/docs/ReleaseNotes.rst
@@ -200,7 +200,13 @@ libclang
 Static Analyzer
 ---------------
 
-...
+- The static analyzer now supports using the
+  `z3 theorem prover <https://github.com/z3prover/z3>`_ from Microsoft Research
+  as an external constraint solver. This allows reasoning over more complex
+  queries, but performance is ~15x slower than the default range-based
+  constraint solver. To enable the z3 solver backend, clang must be built with
+  the ``CLANG_ANALYZER_BUILD_Z3=ON`` option, and the
+  ``-Xanalyzer -analyzer-constraints=z3`` arguments passed at runtime.
 
 Undefined Behavior Sanitizer (UBSan)
 ------------------------------------