diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -2442,15 +2442,15 @@ void FalsePositiveRefutationBRVisitor::finalizeVisitor(
   VisitNode(EndPathNode, BRC, BR);
 
   // Create a refutation manager
-  SMTSolverRef RefutationSolver = CreateZ3Solver();
+  llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
   ASTContext &Ctx = BRC.getASTContext();
 
   // Add constraints to the solver
   for (const auto &I : Constraints) {
     const SymbolRef Sym = I.first;
     auto RangeIt = I.second.begin();
 
-    SMTExprRef Constraints = SMTConv::getRangeExpr(
+    llvm::SMTExprRef Constraints = SMTConv::getRangeExpr(
         RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
         /*InRange=*/true);
     while ((++RangeIt) != I.second.end()) {

diff --git a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
@@ -1,12 +1,5 @@
 set(LLVM_LINK_COMPONENTS support)
 
-# Link Z3 if the user wants to build it.
-if(CLANG_ANALYZER_WITH_Z3)
-  set(Z3_LINK_FILES ${Z3_LIBRARIES})
-else()
-  set(Z3_LINK_FILES "")
-endif()
-
 add_clang_library(clangStaticAnalyzerCore
   APSIntType.cpp
   AnalysisManager.cpp
@@ -46,14 +39,14 @@ add_clang_library(clangStaticAnalyzerCore
   SarifDiagnostics.cpp
   SimpleConstraintManager.cpp
   SimpleSValBuilder.cpp
+  SMTConstraintManager.cpp
   Store.cpp
   SubEngine.cpp
   SValBuilder.cpp
   SVals.cpp
   SymbolManager.cpp
   TaintManager.cpp
   WorkList.cpp
-  Z3ConstraintManager.cpp
 
   LINK_LIBS
   clangAST
@@ -63,12 +56,5 @@ add_clang_library(clangStaticAnalyzerCore
   clangCrossTU
   clangLex
   clangRewrite
-  ${Z3_LINK_FILES}
   )
 
-if(CLANG_ANALYZER_WITH_Z3)
-  target_include_directories(clangStaticAnalyzerCore SYSTEM
-    PRIVATE
-    ${Z3_INCLUDE_DIR}
-    )
-endif()
diff --git a/clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
@@ -0,0 +1,18 @@
+//== SMTConstraintManager.cpp -----------------------------------*- C++ -*--==//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
+
+using namespace clang;
+using namespace ento;
+
+std::unique_ptr<ConstraintManager>
+ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
+  return llvm::make_unique<SMTConstraintManager>(Eng, StMgr.getSValBuilder());
+}
diff --git a/clang/test/CMakeLists.txt b/clang/test/CMakeLists.txt
@@ -144,7 +144,7 @@ if (CLANG_ENABLE_STATIC_ANALYZER)
   set_target_properties(check-clang-analyzer PROPERTIES FOLDER "Clang tests")
 
 
-  if (CLANG_ANALYZER_WITH_Z3)
+  if (LLVM_WITH_Z3)
     add_lit_testsuite(check-clang-analyzer-z3 "Running the Clang analyzer tests, using Z3 as a solver"
       ${CMAKE_CURRENT_BINARY_DIR}/Analysis
       PARAMS ${ANALYZER_TEST_PARAMS_Z3}

diff --git a/clang/test/lit.site.cfg.py.in b/clang/test/lit.site.cfg.py.in
@@ -20,7 +20,7 @@ config.have_zlib = @HAVE_LIBZ@
 config.clang_arcmt = @CLANG_ENABLE_ARCMT@
 config.clang_default_cxx_stdlib = "@CLANG_DEFAULT_CXX_STDLIB@"
 config.clang_staticanalyzer = @CLANG_ENABLE_STATIC_ANALYZER@
-config.clang_staticanalyzer_z3 = "@CLANG_ANALYZER_WITH_Z3@"
+config.clang_staticanalyzer_z3 = "@LLVM_WITH_Z3@"
 config.clang_examples = @CLANG_BUILD_EXAMPLES@
 config.enable_shared = @ENABLE_SHARED@
 config.enable_backtrace = @ENABLE_BACKTRACES@

diff --git a/llvm/CMakeLists.txt b/llvm/CMakeLists.txt
@@ -377,6 +377,31 @@ option(LLVM_ENABLE_THREADS "Use threads if available." ON)
 
 option(LLVM_ENABLE_ZLIB "Use zlib for compression/decompression if available." ON)
 
+set(LLVM_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.")
+
+find_package(Z3 4.7.1)
+
+if (LLVM_Z3_INSTALL_DIR)
+  if (NOT Z3_FOUND)
+    message(FATAL_ERROR "Z3 >= 4.7.1 has not been found in LLVM_Z3_INSTALL_DIR: ${LLVM_Z3_INSTALL_DIR}.")
+  endif()
+endif()
+
+set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")
+
+option(LLVM_ENABLE_Z3_SOLVER
+  "Enable Support for the Z3 constraint solver in LLVM."
+  ${LLVM_ENABLE_Z3_SOLVER_DEFAULT}
+)
+
+if (LLVM_ENABLE_Z3_SOLVER)
+  if (NOT Z3_FOUND)
+    message(FATAL_ERROR "LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.")
+  endif()
+
+  set(LLVM_WITH_Z3 1)
+endif()
+
 if( LLVM_TARGETS_TO_BUILD STREQUAL "all" )
   set( LLVM_TARGETS_TO_BUILD ${LLVM_ALL_TARGETS} )
 endif()

diff --git a/llvm/cmake/modules/FindZ3.cmake b/llvm/cmake/modules/FindZ3.cmake
@@ -0,0 +1,110 @@
+INCLUDE(CheckCXXSourceRuns)
+
+# Function to check Z3's version
+function(check_z3_version z3_include z3_lib)
+  # The program that will be executed to print Z3's version.
+  file(WRITE ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c
+       "#include <assert.h>
+        #include <z3.h>
+        int main() {
+          unsigned int major, minor, build, rev;
+          Z3_get_version(&major, &minor, &build, &rev);
+          printf(\"%u.%u.%u\", major, minor, build);
+          return 0;
+       }")
+
+  # Get lib path
+  get_filename_component(z3_lib_path ${z3_lib} PATH)
+
+  try_run(
+    Z3_RETURNCODE
+    Z3_COMPILED
+    ${CMAKE_BINARY_DIR}
+    ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c
+    COMPILE_DEFINITIONS -I"${z3_include}"
+    LINK_LIBRARIES -L${z3_lib_path} -lz3
+    RUN_OUTPUT_VARIABLE SRC_OUTPUT
+  )
+
+  if(Z3_COMPILED)
+    string(REGEX REPLACE "([0-9]*\\.[0-9]*\\.[0-9]*\\.[0-9]*)" "\\1"
+           z3_version "${SRC_OUTPUT}")
+    set(Z3_VERSION_STRING ${z3_version} PARENT_SCOPE)
+  endif()
+endfunction(check_z3_version)
+
+# Looking for Z3 in LLVM_Z3_INSTALL_DIR
+find_path(Z3_INCLUDE_DIR NAMES z3.h
+  NO_DEFAULT_PATH
+  PATHS ${LLVM_Z3_INSTALL_DIR}/include
+  PATH_SUFFIXES libz3 z3
+  )
+
+find_library(Z3_LIBRARIES NAMES z3 libz3
+  NO_DEFAULT_PATH
+  PATHS ${LLVM_Z3_INSTALL_DIR}
+  PATH_SUFFIXES lib bin
+  )
+
+# If Z3 has not been found in LLVM_Z3_INSTALL_DIR look in the default directories
+find_path(Z3_INCLUDE_DIR NAMES z3.h
+  PATH_SUFFIXES libz3 z3
+  )
+
+find_library(Z3_LIBRARIES NAMES z3 libz3
+  PATH_SUFFIXES lib bin
+  )
+
+# Searching for the version of the Z3 library is a best-effort task
+unset(Z3_VERSION_STRING)
+
+# First, try to check it dynamically, by compiling a small program that
+# prints Z3's version
+if(Z3_INCLUDE_DIR AND Z3_LIBRARIES)
+  # We do not have the Z3 binary to query for a version. Try to use
+  # a small C++ program to detect it via the Z3_get_version() API call.
+  check_z3_version(${Z3_INCLUDE_DIR} ${Z3_LIBRARIES})
+endif()
+
+# If the dynamic check fails, we might be cross compiling: if that's the case,
+# check the version in the headers, otherwise, fail with a message
+if(NOT Z3_VERSION_STRING AND (CMAKE_CROSSCOMPILING AND
+                              Z3_INCLUDE_DIR AND
+                              EXISTS "${Z3_INCLUDE_DIR}/z3_version.h"))
+  # TODO: print message warning that we couldn't find a compatible lib?
+
+  # Z3 4.8.1+ has the version is in a public header.
+  file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
+       z3_version_str REGEX "^#define[\t ]+Z3_MAJOR_VERSION[\t ]+.*")
+  string(REGEX REPLACE "^.*Z3_MAJOR_VERSION[\t ]+([0-9]).*$" "\\1"
+         Z3_MAJOR "${z3_version_str}")
+
+  file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
+       z3_version_str REGEX "^#define[\t ]+Z3_MINOR_VERSION[\t ]+.*")
+  string(REGEX REPLACE "^.*Z3_MINOR_VERSION[\t ]+([0-9]).*$" "\\1"
+         Z3_MINOR "${z3_version_str}")
+
+  file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
+       z3_version_str REGEX "^#define[\t ]+Z3_BUILD_NUMBER[\t ]+.*")
+  string(REGEX REPLACE "^.*Z3_BUILD_VERSION[\t ]+([0-9]).*$" "\\1"
+         Z3_BUILD "${z3_version_str}")
+
+  set(Z3_VERSION_STRING ${Z3_MAJOR}.${Z3_MINOR}.${Z3_BUILD})
+  unset(z3_version_str)
+endif()
+
+if(NOT Z3_VERSION_STRING)
+  # Give up: we are unable to obtain a version of the Z3 library. Be
+  # conservative and force the found version to 0.0.0 to make version
+  # checks always fail.
+  set(Z3_VERSION_STRING "0.0.0")
+endif()
+
+# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if
+# all listed variables are TRUE
+include(FindPackageHandleStandardArgs)
+FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3
+                                  REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR
+                                  VERSION_VAR Z3_VERSION_STRING)
+
+mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES)
diff --git a/llvm/cmake/modules/LLVMConfig.cmake.in b/llvm/cmake/modules/LLVMConfig.cmake.in
@@ -44,6 +44,8 @@ set(LLVM_ENABLE_ZLIB @LLVM_ENABLE_ZLIB@)
 
 set(LLVM_LIBXML2_ENABLED @LLVM_LIBXML2_ENABLED@)
 
+set(LLVM_WITH_Z3 @LLVM_WITH_Z3@)
+
 set(LLVM_ENABLE_DIA_SDK @LLVM_ENABLE_DIA_SDK@)
 
 set(LLVM_NATIVE_ARCH @LLVM_NATIVE_ARCH@)

diff --git a/llvm/include/llvm/Config/config.h.cmake b/llvm/include/llvm/Config/config.h.cmake
@@ -344,6 +344,9 @@
 /* Whether GlobalISel rule coverage is being collected */
 #cmakedefine01 LLVM_GISEL_COV_ENABLED
 
+/* Define if we have z3 and want to build it */
+#cmakedefine LLVM_WITH_Z3 ${LLVM_WITH_Z3}
+
 /* Define to the default GlobalISel coverage file prefix */
 #cmakedefine LLVM_GISEL_COV_PREFIX "${LLVM_GISEL_COV_PREFIX}"
 

diff --git a/...taticAnalyzer/Core/PathSensitive/SMTAPI.h → llvm/include/llvm/Support/SMTAPI.h b/...taticAnalyzer/Core/PathSensitive/SMTAPI.h → llvm/include/llvm/Support/SMTAPI.h
@@ -11,15 +11,16 @@
 //
 //===----------------------------------------------------------------------===//
 
-#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
-#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+#ifndef LLVM_SUPPORT_SMTAPI_H
+#define LLVM_SUPPORT_SMTAPI_H
 
-#include "clang/Basic/TargetInfo.h"
+#include "llvm/ADT/APFloat.h"
 #include "llvm/ADT/APSInt.h"
 #include "llvm/ADT/FoldingSet.h"
+#include "llvm/Support/raw_ostream.h"
+#include <memory>
 
-namespace clang {
-namespace ento {
+namespace llvm {
 
 /// Generic base class for SMT sorts
 class SMTSort {
@@ -399,7 +400,6 @@ using SMTSolverRef = std::shared_ptr<SMTSolver>;
 /// Convenience method to create and Z3Solver object
 SMTSolverRef CreateZ3Solver();
 
-} // namespace ento
-} // namespace clang
+} // namespace llvm
 
 #endif
diff --git a/llvm/lib/Support/CMakeLists.txt b/llvm/lib/Support/CMakeLists.txt
@@ -44,6 +44,13 @@ if (MSVC)
   set (delayload_flags delayimp -delayload:shell32.dll -delayload:ole32.dll)
 endif()
 
+# Link Z3 if the user wants to build it.
+if(LLVM_WITH_Z3)
+  set(Z3_LINK_FILES ${Z3_LIBRARIES})
+else()
+  set(Z3_LINK_FILES "")
+endif()
+
 add_llvm_library(LLVMSupport
   AArch64TargetParser.cpp
   ARMTargetParser.cpp
@@ -152,6 +159,7 @@ add_llvm_library(LLVMSupport
   regfree.c
   regstrlcpy.c
   xxhash.cpp
+  Z3Solver.cpp
 
 # System
   Atomic.cpp
@@ -177,7 +185,14 @@ add_llvm_library(LLVMSupport
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT
   ${LLVM_MAIN_INCLUDE_DIR}/llvm/Support
   ${Backtrace_INCLUDE_DIRS}
-  LINK_LIBS ${system_libs} ${delayload_flags}
+  LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES}
   )
 
 set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}")
+
+if(LLVM_WITH_Z3)
+  target_include_directories(LLVMSupport SYSTEM
+    PRIVATE
+    ${Z3_INCLUDE_DIR}
+    )
+endif()
diff --git a/...aticAnalyzer/Core/Z3ConstraintManager.cpp → llvm/lib/Support/Z3Solver.cpp b/...aticAnalyzer/Core/Z3ConstraintManager.cpp → llvm/lib/Support/Z3Solver.cpp
@@ -1,23 +1,19 @@
-//== Z3ConstraintManager.cpp --------------------------------*- C++ -*--==//
+//== Z3Solver.cpp -----------------------------------------------*- C++ -*--==//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 
-#include "clang/Basic/TargetInfo.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
+#include "llvm/ADT/Twine.h"
+#include "llvm/Config/config.h"
+#include "llvm/Support/SMTAPI.h"
+#include <set>
 
-#include "clang/Config/config.h"
+using namespace llvm;
 
-using namespace clang;
-using namespace ento;
-
-#if CLANG_ANALYZER_WITH_Z3
+#if LLVM_WITH_Z3
 
 #include <z3.h>
 
@@ -818,18 +814,13 @@ class Z3Solver : public SMTSolver {
 
 #endif
 
-SMTSolverRef clang::ento::CreateZ3Solver() {
-#if CLANG_ANALYZER_WITH_Z3
+llvm::SMTSolverRef llvm::CreateZ3Solver() {
+#if LLVM_WITH_Z3
   return llvm::make_unique<Z3Solver>();
 #else
-  llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
-                           "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
+  llvm::report_fatal_error("LLVM was not compiled with Z3 support, rebuild "
+                           "with -DLLVM_ENABLE_Z3_SOLVER=ON",
                            false);
   return nullptr;
 #endif
 }
-
-std::unique_ptr<ConstraintManager>
-ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
-  return llvm::make_unique<SMTConstraintManager>(Eng, StMgr.getSValBuilder());
-}