diff --git a/CMakeLists.txt b/CMakeLists.txt
new file mode 100644
index 000000000..3c10b4f0a
--- /dev/null
+++ b/CMakeLists.txt
@@ -0,0 +1,300 @@
+# This overrides the default flags for the different CMAKE_BUILD_TYPEs
+set(CMAKE_USER_MAKE_RULES_OVERRIDE "${CMAKE_CURRENT_SOURCE_DIR}/cmake/compiler_flags_override.cmake")
+project(Z3 LANGUAGES C CXX)
+cmake_minimum_required(VERSION 2.8.12)
+
+################################################################################
+# Project version
+################################################################################
+set(Z3_VERSION_MAJOR 4)
+set(Z3_VERSION_MINOR 4)
+set(Z3_VERSION_PATCH 2)
+set(Z3_VERSION_TWEAK 0)
+set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
+message(STATUS "Z3 version ${Z3_VERSION}")
+
+################################################################################
+# Message for polluted source tree sanity checks
+################################################################################
+set(z3_polluted_tree_msg
+  " should not exist and is polluting the source tree."
+  " It is likely that this file came from the Python build system which"
+  " generates files inside the source tree. This is bad practice and the CMake"
+  " build system is setup to make sure that the source tree is clean during"
+  " its configure step. If you are using git you can remove all untracked files"
+  " using ``git clean -fx``. Be careful when doing this. You should probably use"
+  " this with ``-n`` first to check which file(s) would be removed."
+)
+
+################################################################################
+# Add our CMake module directory to the list of module search directories
+################################################################################
+list(APPEND CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/cmake/modules")
+
+################################################################################
+# Useful CMake functions/Macros
+################################################################################
+include(CheckCXXSourceCompiles)
+
+################################################################################
+# Compiler flags for Z3 components.
+# Subsequent commands will append to this
+################################################################################
+set(Z3_COMPONENT_CXX_DEFINES "")
+set(Z3_COMPONENT_CXX_FLAGS "")
+set(Z3_COMPONENT_EXTRA_INCLUDE_DIRS "")
+set(Z3_DEPENDENT_LIBS "")
+
+################################################################################
+# Build type
+################################################################################
+message(STATUS "CMake generator: ${CMAKE_GENERATOR}")
+if (DEFINED CMAKE_CONFIGURATION_TYPES)
+  # Multi-configuration build (e.g. Visual Studio and Xcode). Here
+  # CMAKE_BUILD_TYPE doesn't matter
+  message(STATUS "Available configurations: ${CMAKE_CONFIGURATION_TYPES}")
+else()
+  # Single configuration generator (e.g. Unix Makefiles, Ninja)
+  set(available_build_types Debug Release RelWithDebInfo MinSizeRel)
+  if(NOT CMAKE_BUILD_TYPE)
+    message(STATUS "CMAKE_BUILD_TYPE is not set. Setting default")
+    message(STATUS "The available build types are: ${available_build_types}")
+    set(CMAKE_BUILD_TYPE RelWithDebInfo CACHE String
+        "Options are ${build_types}"
+        FORCE)
+    # Provide drop down menu options in cmake-gui
+    set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${available_build_types})
+  endif()
+  message(STATUS "Build type: ${CMAKE_BUILD_TYPE}")
+endif()
+
+# CMAKE_BUILD_TYPE has no meaning for multi-configuration generators
+# (e.g. Visual Studio) so use generator expressions instead to add
+# the right definitions when doing a particular build type.
+#
+# Note for some reason we have to leave off ``-D`` here otherwise
+# we get ``-D-DZ3DEBUG`` passed to the compiler
+list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Debug>:Z3DEBUG>)
+list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Release>:_EXTERNAL_RELEASE>)
+list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:RelWithDebInfo>:_EXTERNAL_RELEASE>)
+
+################################################################################
+# Find Python
+################################################################################
+find_package(PythonInterp REQUIRED)
+message(STATUS "PYTHON_EXECUTABLE: ${PYTHON_EXECUTABLE}")
+
+################################################################################
+# Target architecture detection
+################################################################################
+include(${CMAKE_SOURCE_DIR}/cmake/target_arch_detect.cmake)
+detect_target_architecture(TARGET_ARCHITECTURE)
+message(STATUS "Detected target architecture: ${TARGET_ARCHITECTURE}")
+if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_AMD64_")
+endif()
+
+
+################################################################################
+# Function for detecting C++ compiler flag support
+################################################################################
+include(${CMAKE_SOURCE_DIR}/cmake/z3_add_cxx_flag.cmake)
+
+################################################################################
+# Platform detection
+################################################################################
+if ("${CMAKE_SYSTEM_NAME}" STREQUAL "Linux")
+  message(STATUS "Platform: Linux")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_LINUX_")
+  if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
+    list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL")
+  endif()
+  z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED)
+elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
+  # Does OSX really not need any special flags?
+  message(STATUS "Platform: Darwin")
+elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD")
+  message(STATUS "Platform: FreeBSD")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_")
+  z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED)
+elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD")
+  message(STATUS "Platform: OpenBSD")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_")
+  z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED)
+elseif (CYGWIN)
+  message(STATUS "Platform: Cygwin")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_CYGWIN")
+  z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED)
+elseif (WIN32)
+  message(STATUS "Platform: Windows")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS")
+else()
+  message(FATAL_ERROR "Platform \"${CMAKE_SYSTEM_NAME}\" not recognised")
+endif()
+
+
+################################################################################
+# GNU multiple precision library support
+################################################################################
+option(USE_LIB_GMP "Use GNU Multiple Precision Library" OFF)
+if (USE_LIB_GMP)
+  # Because this is off by default we will make the configure fail if libgmp
+  # can't be found
+  find_package(GMP REQUIRED)
+  message(STATUS "Using libgmp")
+  list(APPEND Z3_DEPENDENT_LIBS ${GMP_C_LIBRARIES})
+  list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS ${GMP_INCLUDE_DIRS})
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_GMP")
+else()
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_INTERNAL")
+  message(STATUS "Not using libgmp")
+endif()
+
+################################################################################
+# FOCI2 support
+################################################################################
+# FIXME: What is this?
+option(USE_FOCI2 "Use FOCI2" OFF)
+if (USE_FOCI2)
+  message(FATAL_ERROR "TODO")
+  message(STATUS "Using FOCI2")
+else()
+  message(STATUS "Not using FOCI2")
+endif()
+
+################################################################################
+# OpenMP support
+################################################################################
+option(USE_OPENMP "Use OpenMP" ON)
+set(OPENMP_FOUND FALSE)
+if (USE_OPENMP)
+  # Because this is on by default we make the configure succeed with a warning
+  # if OpenMP support is not detected.
+  find_package(OpenMP)
+  if (NOT OPENMP_FOUND)
+    message(WARNING "OpenMP support was requested but your compiler doesn't support it")
+  endif()
+endif()
+if (OPENMP_FOUND)
+    list(APPEND Z3_COMPONENT_CXX_FLAGS ${OpenMP_CXX_FLAGS})
+    list(APPEND Z3_DEPENDENT_LIBS ${OpenMP_CXX_FLAGS})
+    unset(CMAKE_REQUIRED_FLAGS)
+    message(STATUS "Using OpenMP")
+else()
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NO_OMP_")
+  message(STATUS "Not using OpenMP")
+endif()
+
+################################################################################
+# FP math
+################################################################################
+# FIXME: Support ARM "-mfpu=vfp -mfloat-abi=hard"
+if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
+  if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
+    set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
+  elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "MSVC")
+    set(SSE_FLAGS "/arch:SSE2")
+  else()
+    message(FATAL_ERROR "Unknown compiler ${CMAKE_CXX_COMPILER_ID}")
+  endif()
+  CHECK_CXX_COMPILER_FLAG("${SSE_FLAGS}" HAS_SSE2)
+  if (HAS_SSE2)
+    list(APPEND Z3_COMPONENT_CXX_FLAGS ${SSE_FLAGS})
+  endif()
+  unset(SSE_FLAGS)
+endif()
+
+################################################################################
+# Compiler warnings
+################################################################################
+include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake)
+
+################################################################################
+# Option to control what type of library we build
+################################################################################
+option(BUILD_LIBZ3_SHARED "Build libz3 as a shared library if true, otherwise build a static library" ON)
+
+
+################################################################################
+# Symbol visibility
+################################################################################
+if (NOT MSVC)
+  z3_add_cxx_flag("-fvisibility=hidden" REQUIRED)
+endif()
+
+################################################################################
+# Tracing
+################################################################################
+option(ENABLE_TRACING OFF "Enable tracing")
+if (ENABLE_TRACING)
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_TRACE")
+endif()
+# Should we always enable tracing when doing a debug build?
+#list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Debug>:_TRACE>)
+
+################################################################################
+# Postion indepdent code
+################################################################################
+# This is required because code built in the components will end up in a shared
+# library. If not building a shared library ``-fPIC`` isn't needed and would add
+# unnecessary overhead.
+if (BUILD_LIBZ3_SHARED)
+  if (NOT MSVC)
+    z3_add_cxx_flag("-fPIC" REQUIRED)
+  endif()
+endif()
+
+################################################################################
+# Report Z3_COMPONENT flags
+################################################################################
+message(STATUS "Z3_COMPONENT_CXX_DEFINES: ${Z3_COMPONENT_CXX_DEFINES}")
+message(STATUS "Z3_COMPONENT_CXX_FLAGS: ${Z3_COMPONENT_CXX_FLAGS}")
+message(STATUS "Z3_DEPENDENT_LIBS: ${Z3_DEPENDENT_LIBS}")
+message(STATUS "Z3_COMPONENT_EXTRA_INCLUDE_DIRS: ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}")
+
+################################################################################
+# Z3 installation locations
+################################################################################
+set (Z3_INSTALL_LIB_DIR "lib")
+set (Z3_INSTALL_BIN_DIR "bin")
+set (Z3_INSTALL_INCLUDE_DIR "include")
+
+################################################################################
+# CMake build file locations
+################################################################################
+# To mimic the python build system output these into the root of the build
+# directory
+set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}")
+set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}")
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}")
+
+################################################################################
+# Z3 components, library and executables
+################################################################################
+include(${CMAKE_SOURCE_DIR}/cmake/z3_add_component.cmake)
+add_subdirectory(src)
+
+################################################################################
+# Examples
+################################################################################
+option(ENABLE_EXAMPLE_TARGETS "Build Z3 api examples" ON)
+if (ENABLE_EXAMPLE_TARGETS)
+  add_subdirectory(examples)
+endif()
+
+################################################################################
+# Uninstall rule
+################################################################################
+configure_file(
+  "${CMAKE_SOURCE_DIR}/cmake/cmake_uninstall.cmake.in"
+  "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
+  @ONLY
+)
+
+add_custom_target(uninstall
+  COMMAND
+  "${CMAKE_COMMAND}" -P "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
+  COMMENT "Uninstalling..."
+  USES_TERMINAL
+  VERBATIM
+)
diff --git a/cmake/cmake_uninstall.cmake.in b/cmake/cmake_uninstall.cmake.in
new file mode 100644
index 000000000..cbe8c2749
--- /dev/null
+++ b/cmake/cmake_uninstall.cmake.in
@@ -0,0 +1,24 @@
+if(NOT EXISTS "@CMAKE_CURRENT_BINARY_DIR@/install_manifest.txt")
+  message(FATAL_ERROR "Cannot find install manifest: "
+          "@CMAKE_CURRENT_BINARY_DIR@/install_manifest.txt")
+endif()
+
+file(READ "@CMAKE_CURRENT_BINARY_DIR@/install_manifest.txt" files)
+string(REGEX REPLACE "\n" ";" files "${files}")
+foreach(file ${files})
+  set(_full_file_path "$ENV{DESTDIR}${file}")
+  message(STATUS "Uninstalling ${_full_file_path}")
+  if(IS_SYMLINK "${_full_file_path}" OR EXISTS "${_full_file_path}")
+    # We could use ``file(REMOVE ...)`` here but then we wouldn't
+    # know if the removal failed.
+    execute_process(COMMAND
+      "@CMAKE_COMMAND@" "-E" "remove" "${_full_file_path}"
+      RESULT_VARIABLE rm_retval
+    )
+    if(NOT "${rm_retval}" STREQUAL 0)
+      message(FATAL_ERROR "Problem when removing \"${_full_file_path}\"")
+    endif()
+  else()
+    message(STATUS "File \"${_full_file_path}\" does not exist.")
+  endif()
+endforeach()
diff --git a/cmake/compiler_flags_override.cmake b/cmake/compiler_flags_override.cmake
new file mode 100644
index 000000000..cb1f8dbc1
--- /dev/null
+++ b/cmake/compiler_flags_override.cmake
@@ -0,0 +1,30 @@
+# This file overrides the default compiler flags for CMake's built-in
+# configurations (CMAKE_BUILD_TYPE). Most compiler flags should not be set here.
+# The main purpose is to make sure ``-DNDEBUG`` is never set by default.
+if (CMAKE_C_COMPILER_ID)
+  set(_lang C)
+elseif(CMAKE_CXX_COMPILER_ID)
+  set(_lang CXX)
+else()
+  message(FATAL_ERROR "Unknown language")
+endif()
+
+if (("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "GNU"))
+  # Taken from Modules/Compiler/GNU.cmake but -DNDEBUG is removed
+  set(CMAKE_${_lang}_FLAGS_INIT "")
+  # FIXME: should we have -D_DEBUG here to match MSVC build?
+  set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "-g -O0")
+  set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "-Os")
+  set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "-O3")
+  set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "-O2 -g")
+elseif ("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "MSVC")
+  # Not tested!
+  set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "/D_DEBUG /MTd /Zi /Ob0 /Od /RTC1")
+  set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT     "/MT /O1 /Ob1")
+  set(CMAKE_${_lang}_FLAGS_RELEASE_INIT        "/MT /O2 /Ob2")
+  set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "/MT /Zi /O2 /Ob1")
+else()
+  message(FATAL_ERROR "Overrides not set for ${_lang} compiler \"${CMAKE_${_lang}_COMPILER_ID}\"")
+endif()
+
+unset(_lang)
diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake
new file mode 100644
index 000000000..e9910c2e4
--- /dev/null
+++ b/cmake/compiler_warnings.cmake
@@ -0,0 +1,38 @@
+set(GCC_AND_CLANG_WARNINGS
+    "-Wall"
+)
+set(GCC_ONLY_WARNINGS "")
+set(CLANG_ONLY_WARNINGS "")
+set(MSVC_WARNINGS "/W3")
+
+set(WARNING_FLAGS_TO_CHECK "")
+if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")
+  list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS})
+  list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS})
+elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
+  list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS})
+  list(APPEND WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS})
+elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "MSVC")
+  list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS})
+else()
+  message(AUTHOR_WARNING "Unknown compiler")
+endif()
+
+# Loop through flags and use the ones which the compiler supports
+foreach (flag ${WARNING_FLAGS_TO_CHECK})
+  z3_add_cxx_flag("${flag}")
+endforeach()
+
+option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" OFF)
+if (WARNINGS_AS_ERRORS)
+  if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
+    list(APPEND Z3_COMPONENT_CXX_FLAGS "-Werror")
+  elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "MSVC")
+    list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX")
+  else()
+    message(AUTHOR_WARNING "Unknown compiler")
+  endif()
+  message(STATUS "Treating compiler warnings as errors")
+else()
+  message(STATUS "Not treating compiler warnings as errors")
+endif()
diff --git a/cmake/modules/FindGMP.cmake b/cmake/modules/FindGMP.cmake
new file mode 100644
index 000000000..b749750ef
--- /dev/null
+++ b/cmake/modules/FindGMP.cmake
@@ -0,0 +1,64 @@
+# Tries to find an install of the GNU multiple precision library
+#
+# Once done this will define
+#  GMP_FOUND - BOOL: System has the GMP library installed
+#  GMP_INCLUDE_DIRS - LIST:The GMP include directories
+#  GMP_C_LIBRARIES - LIST:The libraries needed to use GMP via it's C interface
+#  GMP_CXX_LIBRARIES - LIST:The libraries needed to use GMP via it's C++ interface
+
+include(FindPackageHandleStandardArgs)
+
+# Try to find libraries
+find_library(GMP_C_LIBRARIES
+  NAMES gmp
+  DOC "GMP C libraries"
+)
+if (GMP_C_LIBRARIES)
+  message(STATUS "Found GMP C library: \"${GMP_C_LIBRARIES}\"")
+else()
+  message(STATUS "Could not find GMP C library")
+endif()
+find_library(GMP_CXX_LIBRARIES
+  NAMES gmpxx
+  DOC "GMP C++ libraries"
+)
+if (GMP_CXX_LIBRARIES)
+  message(STATUS "Found GMP C++ library: \"${GMP_CXX_LIBRARIES}\"")
+else()
+  message(STATUS "Could not find GMP C++ library")
+endif()
+
+# Try to find headers
+find_path(GMP_C_INCLUDES
+  NAMES gmp.h
+  DOC "GMP C header"
+)
+if (GMP_C_INCLUDES)
+  message(STATUS "Found GMP C include path: \"${GMP_C_INCLUDES}\"")
+else()
+  message(STATUS "Could not find GMP C include path")
+endif()
+
+find_path(GMP_CXX_INCLUDES
+  NAMES gmpxx.h
+  DOC "GMP C++ header"
+)
+if (GMP_CXX_INCLUDES)
+  message(STATUS "Found GMP C++ include path: \"${GMP_CXX_INCLUDES}\"")
+else()
+  message(STATUS "Could not find GMP C++ include path")
+endif()
+
+if (GMP_C_LIBRARIES AND GMP_CXX_LIBRARIES AND GMP_C_INCLUDES AND GMP_CXX_INCLUDES)
+  set(GMP_INCLUDE_DIRS "${GMP_C_INCLUDES}" "${GMP_CXX_INCLUDES}")
+  list(REMOVE_DUPLICATES GMP_INCLUDE_DIRS)
+  message(STATUS "Found GMP")
+else()
+  message(STATUS "Could not find GMP")
+endif()
+
+# TODO: We should check we can link some simple code against libgmp and libgmpxx
+
+# Handle QUIET and REQUIRED and check the necessary variables were set and if so
+# set ``GMP_FOUND``
+find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIRS GMP_C_LIBRARIES GMP_CXX_LIBRARIES)
diff --git a/cmake/target_arch_detect.cmake b/cmake/target_arch_detect.cmake
new file mode 100644
index 000000000..68194cfe4
--- /dev/null
+++ b/cmake/target_arch_detect.cmake
@@ -0,0 +1,22 @@
+###############################################################################
+# Target detection
+#
+# We abuse the compiler preprocessor to work out what target the compiler is
+# building for. The nice thing about this approach is that we'll detect the
+# right target even if we are using a cross compiler.
+###############################################################################
+function(detect_target_architecture OUTPUT_VAR)
+  try_run(run_result
+    compile_result
+    "${CMAKE_BINARY_DIR}"
+    "${CMAKE_SOURCE_DIR}/cmake/target_arch_detect.cpp"
+    COMPILE_OUTPUT_VARIABLE compiler_output
+  )
+  if (compile_result)
+    message(FATAL_ERROR "Expected compile to fail")
+  endif()
+  string(REGEX MATCH "CMAKE_TARGET_ARCH_([a-zA-Z0-9_]+)" arch "${compiler_output}")
+  # Strip out prefix
+  string(REPLACE "CMAKE_TARGET_ARCH_" "" arch "${arch}")
+  set(${OUTPUT_VAR} "${arch}" PARENT_SCOPE)
+endfunction()
diff --git a/cmake/target_arch_detect.cpp b/cmake/target_arch_detect.cpp
new file mode 100644
index 000000000..8053e3532
--- /dev/null
+++ b/cmake/target_arch_detect.cpp
@@ -0,0 +1,10 @@
+// This is used by the CMake build to detect
+// what architecture the compiler is targeting.
+// TODO: Add more targets here
+#if defined(__i386__) || defined(_M_IX86)
+#error CMAKE_TARGET_ARCH_i686
+#elif defined(__x86_64__) || defined(_M_X64)
+#error CMAKE_TARGET_ARCH_x86_64
+#else
+#error CMAKE_TARGET_ARCH_unknown
+#endif
diff --git a/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake
new file mode 100644
index 000000000..565674055
--- /dev/null
+++ b/cmake/z3_add_component.cmake
@@ -0,0 +1,245 @@
+include(CMakeParseArguments)
+define_property(GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS
+                BRIEF_DOCS "List of Z3 components to use in libz3"
+                FULL_DOCS "List of Z3 components to use in libz3")
+
+function(z3_expand_dependencies output_var)
+  if (ARGC LESS 2)
+    message(FATAL_ERROR "Invalid number of arguments")
+  endif()
+  # Remaing args should be component names
+  set(_expanded_deps ${ARGN})
+  set(_old_number_of_deps 0)
+  list(LENGTH _expanded_deps _number_of_deps)
+  while (_number_of_deps GREATER _old_number_of_deps)
+    set(_old_number_of_deps "${_number_of_deps}")
+    # Loop over the known dependencies and retrieve their dependencies
+    set(_old_expanded_deps ${_expanded_deps})
+    foreach (dependency ${_old_expanded_deps})
+      get_property(_depdeps GLOBAL PROPERTY Z3_${dependency}_DEPS)
+      list(APPEND _expanded_deps ${_depdeps})
+      unset(_depdeps)
+    endforeach()
+    list(REMOVE_DUPLICATES _expanded_deps)
+    list(LENGTH _expanded_deps _number_of_deps)
+  endwhile()
+  set(${output_var} ${_expanded_deps} PARENT_SCOPE)
+endfunction()
+
+function(z3_add_component_dependencies_to_target target_name)
+  if (ARGC LESS 2)
+    message(FATAL_ERROR "Invalid number of arguments")
+  endif()
+  if (NOT (TARGET ${target_name}))
+    message(FATAL_ERROR "Target \"${target_name}\" does not exist")
+  endif()
+  # Remaing args should be component names
+  set(_expanded_deps ${ARGN})
+  foreach (dependency ${_expanded_deps})
+    # FIXME: Adding these include paths wouldn't be necessary if the sources
+    # used include paths rooted in the ``src`` directory.
+    get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
+    foreach (inc_dir ${_dep_include_dirs})
+      target_include_directories(${target_name} PRIVATE "${inc_dir}")
+    endforeach()
+    unset(_dep_include_dirs)
+    # Ensure this component's dependencies are built before this component.
+    # This important because we might need the generated header files in
+    # other components.
+    add_dependencies(${target_name} ${dependency})
+  endforeach()
+endfunction()
+
+macro(z3_add_component component_name)
+  CMAKE_PARSE_ARGUMENTS("Z3_MOD" "NOT_LIBZ3_COMPONENT" "" "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES" ${ARGN})
+  message(STATUS "Adding component ${component_name}")
+  # Note: We don't check the sources exist here because
+  # they might be generated files that don't exist yet.
+
+  set(_list_generated_headers "")
+  foreach (pyg_file ${Z3_MOD_PYG_FILES})
+    set(_full_pyg_file_path "${CMAKE_CURRENT_SOURCE_DIR}/${pyg_file}")
+    if (NOT (EXISTS "${_full_pyg_file_path}"))
+      message(FATAL_ERROR "\"${_full_pyg_file_path}\" does not exist")
+    endif()
+    string(REPLACE ".pyg" ".hpp" _output_file "${pyg_file}")
+    if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${_output_file}")
+      message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${_output_file}\" "
+        ${z3_polluted_tree_msg}
+      )
+    endif()
+    set(_full_output_file_path "${CMAKE_CURRENT_BINARY_DIR}/${_output_file}")
+    message(STATUS "Adding rule to generate \"${_output_file}\"")
+    add_custom_command(OUTPUT "${_output_file}"
+      COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/scripts/pyg2hpp.py" "${_full_pyg_file_path}" "${CMAKE_CURRENT_BINARY_DIR}"
+      MAIN_DEPENDENCY "${_full_pyg_file_path}"
+      DEPENDS "${CMAKE_SOURCE_DIR}/scripts/pyg2hpp.py" "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+      COMMENT "Generating \"${_full_output_file_path}\" from \"${pyg_file}\""
+      WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}"
+      USES_TERMINAL
+      VERBATIM
+    )
+    list(APPEND _list_generated_headers "${_full_output_file_path}")
+  endforeach()
+  unset(_full_include_dir_path)
+  unset(_full_output_file_path)
+  unset(_output_file)
+
+  # Using "object" libraries here means we have a convenient
+  # name to refer to a component in CMake but we don't actually
+  # create a static/library from them. This allows us to easily
+  # build a static or dynamic library from the object libraries
+  # on all platforms. Is this added flexibility worth the linking
+  # overhead it adds?
+  add_library(${component_name} OBJECT ${Z3_MOD_SOURCES} ${_list_generated_headers})
+  unset(_list_generated_headers)
+  # Add definitions
+  foreach (define ${Z3_COMPONENT_CXX_DEFINES})
+    target_compile_definitions(${component_name} PRIVATE ${define})
+  endforeach()
+  # Add compiler flags
+  foreach (flag ${Z3_COMPONENT_CXX_FLAGS})
+    target_compile_options(${component_name} PRIVATE ${flag})
+  endforeach()
+
+  # It's unfortunate that we have to manage the include directories and dependencies ourselves.
+  #
+  # If we weren't building "object" libraries we could use
+  # ```
+  # target_include_directories(${component_name} INTERFACE "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
+  # target_link_libraries(${component_name} INTERFACE ${Z3_MOD_COMPONENT_DEPENDENCIES})
+  # ```
+  # but we can't do that with "object" libraries.
+
+  # Record this component's include directories
+  set_property(GLOBAL PROPERTY Z3_${component_name}_INCLUDES "${CMAKE_CURRENT_SOURCE_DIR}")
+  set_property(GLOBAL APPEND PROPERTY Z3_${component_name}_INCLUDES "${CMAKE_CURRENT_BINARY_DIR}")
+  set_property(GLOBAL PROPERTY Z3_${component_name}_DEPS "")
+  # Record this component's dependencies
+  foreach (dependency ${Z3_MOD_COMPONENT_DEPENDENCIES})
+    if (NOT (TARGET ${dependency}))
+      message(FATAL_ERROR "Component \"${component_name}\" depends on a non existant component \"${dependency}\"")
+    endif()
+    set_property(GLOBAL APPEND PROPERTY Z3_${component_name}_DEPS "${dependency}")
+  endforeach()
+
+  # Determine all the components that this component depends on
+  set(_expanded_deps "")
+  if (DEFINED Z3_MOD_COMPONENT_DEPENDENCIES)
+    z3_expand_dependencies(_expanded_deps ${Z3_MOD_COMPONENT_DEPENDENCIES})
+    z3_add_component_dependencies_to_target(${component_name} ${_expanded_deps})
+  endif()
+  #message(STATUS "Component \"${component_name}\" has the following dependencies ${_expanded_deps}")
+
+  # For any generated header files for this component
+  target_include_directories(${component_name} PRIVATE "${CMAKE_CURRENT_BINARY_DIR}")
+  # So that any generated header files can refer to source files in the component's
+  # source tree
+  target_include_directories(${component_name} PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}")
+
+  # Add any extra include directories
+  foreach (extra_include ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
+    target_include_directories(${component_name} PRIVATE "${extra_include}")
+  endforeach()
+
+  if (NOT Z3_MOD_NOT_LIBZ3_COMPONENT)
+    # Add this component to the global list of Z3 components for libz3
+    set_property(GLOBAL APPEND PROPERTY Z3_LIBZ3_COMPONENTS ${component_name})
+  endif()
+endmacro()
+
+macro(z3_add_install_tactic_rule)
+  # Arguments should be component names to use
+  if (ARGC LESS 1)
+    message(FATAL_ERROR "There should be at least one component")
+  endif()
+  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/install_tactic.cpp")
+    message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/install_tactic.cpp\""
+            ${z3_polluted_tree_msg}
+    )
+  endif()
+  z3_expand_dependencies(_expanded_components ${ARGN})
+  # Get paths to search
+  set(_search_paths "")
+  foreach (dependency ${_expanded_components})
+    get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
+    list(APPEND _search_paths ${_dep_include_dirs})
+  endforeach()
+  list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
+  add_custom_command(OUTPUT "install_tactic.cpp"
+    COMMAND "${PYTHON_EXECUTABLE}"
+    "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
+    "${CMAKE_CURRENT_BINARY_DIR}"
+    ${_search_paths}
+    DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
+            "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+            ${_expanded_components}
+    COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\""
+    USES_TERMINAL
+    VERBATIM
+  )
+endmacro()
+
+macro(z3_add_memory_initializer_rule)
+  # Arguments should be component names to use
+  if (ARGC LESS 1)
+    message(FATAL_ERROR "There should be at least one component")
+  endif()
+  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/mem_initializer.cpp")
+    message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/mem_initializer.cpp\""
+            ${z3_polluted_tree_msg}
+    )
+  endif()
+  z3_expand_dependencies(_expanded_components ${ARGN})
+  # Get paths to search
+  set(_search_paths "")
+  foreach (dependency ${_expanded_components})
+    get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
+    list(APPEND _search_paths ${_dep_include_dirs})
+  endforeach()
+  list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
+  add_custom_command(OUTPUT "mem_initializer.cpp"
+    COMMAND "${PYTHON_EXECUTABLE}"
+    "${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py"
+    "${CMAKE_CURRENT_BINARY_DIR}"
+    ${_search_paths}
+    DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py"
+            "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+            ${_expanded_components}
+    COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp\""
+    USES_TERMINAL
+    VERBATIM
+  )
+endmacro()
+
+macro(z3_add_gparams_register_modules_rule)
+  # Arguments should be component names to use
+  if (ARGC LESS 1)
+    message(FATAL_ERROR "There should be at least one component")
+  endif()
+  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/gparams_register_modules.cpp")
+    message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/gparams_register_modules.cpp\""
+            ${z3_polluted_tree_msg}
+    )
+  endif()
+  z3_expand_dependencies(_expanded_components ${ARGN})
+  # Get paths to search
+  set(_search_paths "")
+  foreach (dependency ${_expanded_components})
+    get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
+    list(APPEND _search_paths ${_dep_include_dirs})
+  endforeach()
+  list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
+  add_custom_command(OUTPUT "gparams_register_modules.cpp"
+    COMMAND "${PYTHON_EXECUTABLE}"
+    "${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py"
+    "${CMAKE_CURRENT_BINARY_DIR}"
+    ${_search_paths}
+    DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py"
+            "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+            ${_expanded_components}
+    COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp\""
+    USES_TERMINAL
+    VERBATIM
+  )
+endmacro()
diff --git a/cmake/z3_add_cxx_flag.cmake b/cmake/z3_add_cxx_flag.cmake
new file mode 100644
index 000000000..0c56bb0f6
--- /dev/null
+++ b/cmake/z3_add_cxx_flag.cmake
@@ -0,0 +1,22 @@
+include(CheckCXXCompilerFlag)
+include(CMakeParseArguments)
+
+function(z3_add_cxx_flag flag)
+  CMAKE_PARSE_ARGUMENTS(z3_add_flag "REQUIRED" "" "" ${ARGN})
+  string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}")
+  string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  unset(HAS_${SANITIZED_FLAG_NAME})
+  CHECK_CXX_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME})
+  if (z3_add_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME})
+    message(FATAL_ERROR "The flag \"${flag}\" is required but your C++ compiler doesn't support it")
+  endif()
+  if (HAS_${SANITIZED_FLAG_NAME})
+    message(STATUS "C++ compiler supports ${flag}")
+    list(APPEND Z3_COMPONENT_CXX_FLAGS "${flag}")
+    set(Z3_COMPONENT_CXX_FLAGS "${Z3_COMPONENT_CXX_FLAGS}" PARENT_SCOPE)
+  else()
+    message(STATUS "C++ compiler does not support ${flag}")
+  endif()
+endfunction()
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
new file mode 100644
index 000000000..b8cecbe63
--- /dev/null
+++ b/examples/CMakeLists.txt
@@ -0,0 +1,2 @@
+add_subdirectory(c)
+add_subdirectory(c++)
diff --git a/examples/c++/CMakeLists.txt b/examples/c++/CMakeLists.txt
new file mode 100644
index 000000000..85bbd77c7
--- /dev/null
+++ b/examples/c++/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_executable(cpp_example EXCLUDE_FROM_ALL example.cpp)
+target_link_libraries(cpp_example PRIVATE libz3)
+target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api")
+target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api/c++")
diff --git a/examples/c/CMakeLists.txt b/examples/c/CMakeLists.txt
new file mode 100644
index 000000000..1a14573ac
--- /dev/null
+++ b/examples/c/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_executable(c_example EXCLUDE_FROM_ALL test_capi.c)
+target_link_libraries(c_example PRIVATE libz3)
+target_include_directories(c_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api")
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
new file mode 100644
index 000000000..4a41cccec
--- /dev/null
+++ b/src/CMakeLists.txt
@@ -0,0 +1,139 @@
+# I'm duplicating the order in ``mk_project.py`` for now to help us keep
+# the build systems in sync.
+#
+# The components in these directory explicitly declare their dependencies so
+# you may be able to re-order some of these directories but an error will be
+# raised if you try to declare a component is depedent on another component
+# that has not yet been declared.
+add_subdirectory(util)
+add_subdirectory(math/polynomial)
+add_subdirectory(sat)
+add_subdirectory(nlsat)
+add_subdirectory(math/hilbert)
+add_subdirectory(math/simplex)
+add_subdirectory(math/automata)
+add_subdirectory(math/interval)
+add_subdirectory(math/realclosure)
+add_subdirectory(math/subpaving)
+add_subdirectory(ast)
+add_subdirectory(ast/rewriter)
+add_subdirectory(ast/normal_forms)
+add_subdirectory(model)
+add_subdirectory(tactic)
+add_subdirectory(ast/substitution)
+add_subdirectory(parsers/util)
+add_subdirectory(math/grobner)
+add_subdirectory(math/euclid)
+add_subdirectory(tactic/core)
+add_subdirectory(sat/tactic)
+add_subdirectory(tactic/arith)
+add_subdirectory(nlsat/tactic)
+add_subdirectory(math/subpaving/tactic)
+add_subdirectory(tactic/aig)
+add_subdirectory(solver)
+add_subdirectory(ackermannization)
+add_subdirectory(interp)
+add_subdirectory(cmd_context)
+add_subdirectory(cmd_context/extra_cmds)
+add_subdirectory(parsers/smt2)
+add_subdirectory(ast/proof_checker)
+## Simplifier module will be deleted in the future.
+## It has been replaced with rewriter component.
+add_subdirectory(ast/simplifier)
+add_subdirectory(ast/fpa)
+add_subdirectory(ast/macros)
+add_subdirectory(ast/pattern)
+add_subdirectory(ast/rewriter/bit_blaster)
+add_subdirectory(smt/params)
+add_subdirectory(smt/proto_model)
+add_subdirectory(smt)
+add_subdirectory(tactic/bv)
+add_subdirectory(smt/tactic)
+add_subdirectory(tactic/sls)
+add_subdirectory(qe)
+add_subdirectory(duality)
+add_subdirectory(muz/base)
+add_subdirectory(muz/dataflow)
+add_subdirectory(muz/transforms)
+add_subdirectory(muz/rel)
+add_subdirectory(muz/pdr)
+add_subdirectory(muz/clp)
+add_subdirectory(muz/tab)
+add_subdirectory(muz/bmc)
+add_subdirectory(muz/ddnf)
+add_subdirectory(muz/duality)
+add_subdirectory(muz/fp)
+add_subdirectory(tactic/nlsat_smt)
+add_subdirectory(tactic/ufbv)
+add_subdirectory(sat/sat_solver)
+add_subdirectory(tactic/smtlogics)
+add_subdirectory(tactic/fpa)
+add_subdirectory(tactic/portfolio)
+add_subdirectory(parsers/smt)
+add_subdirectory(opt)
+add_subdirectory(api)
+add_subdirectory(api/dll)
+
+################################################################################
+# libz3
+################################################################################
+get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS)
+set (object_files "")
+foreach (component ${Z3_LIBZ3_COMPONENTS_LIST})
+  list(APPEND object_files $<TARGET_OBJECTS:${component}>)
+endforeach()
+if (BUILD_LIBZ3_SHARED)
+  set(lib_type "SHARED")
+else()
+  set(lib_type "STATIC")
+endif()
+add_library(libz3 ${lib_type} ${object_files})
+# FIXME: Set "VERSION" and "SOVERSION" properly
+set_target_properties(libz3 PROPERTIES
+  OUTPUT_NAME z3
+  # FIXME: Should we be using ${Z3_VERSION} here?
+  # VERSION: Sets up symlinks, does it do anything else?
+  VERSION ${Z3_VERSION}
+  # SOVERSION: On platforms that use ELF this sets the API version
+  # and should be incremented everytime the API changes
+  SOVERSION ${Z3_VERSION})
+
+# Using INTERFACE means that targets that try link against libz3 will
+# automatically link against the libs in Z3_DEPENDENT_LIBS
+target_link_libraries(libz3 INTERFACE ${Z3_DEPENDENT_LIBS})
+# Declare which header file are the public header files of libz3
+# these will automatically installed when the libz3 target is installed
+set (libz3_public_headers
+  z3_algebraic.h
+  z3_api.h
+  z3_ast_containers.h
+  z3_fixedpoint.h
+  z3_fpa.h
+  z3.h
+  c++/z3++.h
+  z3_interp.h
+  z3_macros.h
+  z3_optimization.h
+  z3_polynomial.h
+  z3_rcf.h
+  z3_v1.h
+)
+foreach (header ${libz3_public_headers})
+  set_property(TARGET libz3 APPEND PROPERTY
+    PUBLIC_HEADER "${CMAKE_SOURCE_DIR}/src/api/${header}")
+endforeach()
+
+install(TARGETS libz3
+  LIBRARY DESTINATION "${Z3_INSTALL_LIB_DIR}"
+  ARCHIVE DESTINATION "${Z3_INSTALL_LIB_DIR}"
+  PUBLIC_HEADER DESTINATION "${Z3_INSTALL_INCLUDE_DIR}"
+)
+################################################################################
+# Z3 executable
+################################################################################
+add_subdirectory(shell)
+
+################################################################################
+# z3-test
+################################################################################
+add_subdirectory(test)
diff --git a/src/ackermannization/CMakeLists.txt b/src/ackermannization/CMakeLists.txt
new file mode 100644
index 000000000..93529ae12
--- /dev/null
+++ b/src/ackermannization/CMakeLists.txt
@@ -0,0 +1,20 @@
+z3_add_component(ackermannization
+  SOURCES
+    ackermannize_bv_model_converter.cpp
+    ackermannize_bv_tactic.cpp
+    ackr_bound_probe.cpp
+    ackr_helper.cpp
+    ackr_model_converter.cpp
+    lackr.cpp
+    lackr_model_constructor.cpp
+    lackr_model_converter_lazy.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    model
+    rewriter
+    solver
+    tactic
+  PYG_FILES
+    ackermannization_params.pyg
+    ackermannize_bv_tactic_params.pyg
+)
diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt
new file mode 100644
index 000000000..506b28cb3
--- /dev/null
+++ b/src/api/CMakeLists.txt
@@ -0,0 +1,86 @@
+set(api_header_files_to_scan
+  z3_api.h
+  z3_ast_containers.h
+  z3_algebraic.h
+  z3_polynomial.h
+  z3_rcf.h
+  z3_fixedpoint.h
+  z3_optimization.h
+  z3_interp.h
+  z3_fpa.h
+)
+set(generated_files
+  api_commands.cpp
+  api_log_macros.cpp
+  api_log_macros.h
+)
+
+# Sanity check
+foreach (gen_file ${generated_files})
+  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${gen_file}")
+    message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${gen_files}\""
+            ${z3_polluted_tree_msg})
+  endif()
+endforeach()
+
+set(full_path_api_header_files_to_scan "")
+foreach (header_file ${api_header_files_to_scan})
+  list(APPEND full_path_api_header_files_to_scan "${CMAKE_CURRENT_SOURCE_DIR}/${header_file}")
+endforeach()
+set(full_path_generated_files "")
+foreach (gen_file ${generated_files})
+  list(APPEND full_path_generated_files "${CMAKE_CURRENT_BINARY_DIR}/${gen_file}")
+endforeach()
+
+add_custom_command(OUTPUT ${generated_files}
+  COMMAND "${PYTHON_EXECUTABLE}"
+  "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
+  "${CMAKE_CURRENT_BINARY_DIR}"
+  ${full_path_api_header_files_to_scan}
+  DEPENDS "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
+          "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+          ${full_path_api_header_files_to_scan}
+  COMMENT "Generating ${generated_files}"
+  USES_TERMINAL
+  VERBATIM
+)
+
+z3_add_component(api
+  SOURCES
+    api_algebraic.cpp
+    api_arith.cpp
+    api_array.cpp
+    api_ast.cpp
+    api_ast_map.cpp
+    api_ast_vector.cpp
+    api_bv.cpp
+    api_config_params.cpp
+    api_context.cpp
+    api_datalog.cpp
+    api_datatype.cpp
+    api_fpa.cpp
+    api_goal.cpp
+    api_interp.cpp
+    api_log.cpp
+    api_model.cpp
+    api_numeral.cpp
+    api_opt.cpp
+    api_params.cpp
+    api_parsers.cpp
+    api_pb.cpp
+    api_polynomial.cpp
+    api_quant.cpp
+    api_rcf.cpp
+    api_seq.cpp
+    api_solver.cpp
+    api_stats.cpp
+    api_tactic.cpp
+    z3_replayer.cpp
+    ${full_path_generated_files}
+  COMPONENT_DEPENDENCIES
+    interp
+    opt
+    portfolio
+    realclosure
+    smtparser
+)
diff --git a/src/api/dll/CMakeLists.txt b/src/api/dll/CMakeLists.txt
new file mode 100644
index 000000000..31b0fb576
--- /dev/null
+++ b/src/api/dll/CMakeLists.txt
@@ -0,0 +1,13 @@
+set(api_dll_deps api extra_cmds sat)
+z3_add_component(api_dll
+  SOURCES
+    dll.cpp
+    "${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp"
+    "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp"
+    "${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp"
+  COMPONENT_DEPENDENCIES
+    ${api_dll_deps}
+)
+z3_add_install_tactic_rule(${api_dll_deps})
+z3_add_memory_initializer_rule(${api_dll_deps})
+z3_add_gparams_register_modules_rule(${api_dll_deps})
diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt
new file mode 100644
index 000000000..de0e4bdaf
--- /dev/null
+++ b/src/ast/CMakeLists.txt
@@ -0,0 +1,48 @@
+z3_add_component(ast
+  SOURCES
+    act_cache.cpp
+    arith_decl_plugin.cpp
+    array_decl_plugin.cpp
+    ast.cpp
+    ast_ll_pp.cpp
+    ast_lt.cpp
+    ast_pp_util.cpp
+    ast_printer.cpp
+    ast_smt2_pp.cpp
+    ast_smt_pp.cpp
+    ast_translation.cpp
+    ast_util.cpp
+    bv_decl_plugin.cpp
+    datatype_decl_plugin.cpp
+    decl_collector.cpp
+    dl_decl_plugin.cpp
+    expr2polynomial.cpp
+    expr2var.cpp
+    expr_abstract.cpp
+    expr_functors.cpp
+    expr_map.cpp
+    expr_stat.cpp
+    expr_substitution.cpp
+    for_each_ast.cpp
+    for_each_expr.cpp
+    format.cpp
+    fpa_decl_plugin.cpp
+    func_decl_dependencies.cpp
+    has_free_vars.cpp
+    macro_substitution.cpp
+    num_occurs.cpp
+    occurs.cpp
+    pb_decl_plugin.cpp
+    pp.cpp
+    reg_decl_plugins.cpp
+    seq_decl_plugin.cpp
+    shared_occs.cpp
+    static_features.cpp
+    used_vars.cpp
+    well_sorted.cpp
+  COMPONENT_DEPENDENCIES
+    polynomial
+    util # Unnecessary? polynomial already depends on util
+  PYG_FILES
+    pp_params.pyg
+)
diff --git a/src/ast/fpa/CMakeLists.txt b/src/ast/fpa/CMakeLists.txt
new file mode 100644
index 000000000..12298b573
--- /dev/null
+++ b/src/ast/fpa/CMakeLists.txt
@@ -0,0 +1,10 @@
+z3_add_component(fpa
+  SOURCES
+    fpa2bv_converter.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    simplifier
+    util
+  PYG_FILES
+    fpa2bv_rewriter_params.pyg
+)
diff --git a/src/ast/macros/CMakeLists.txt b/src/ast/macros/CMakeLists.txt
new file mode 100644
index 000000000..ca38b4759
--- /dev/null
+++ b/src/ast/macros/CMakeLists.txt
@@ -0,0 +1,9 @@
+z3_add_component(macros
+  SOURCES
+    macro_finder.cpp
+    macro_manager.cpp
+    macro_util.cpp
+    quasi_macros.cpp
+  COMPONENT_DEPENDENCIES
+    simplifier
+)
diff --git a/src/ast/normal_forms/CMakeLists.txt b/src/ast/normal_forms/CMakeLists.txt
new file mode 100644
index 000000000..30702cd8c
--- /dev/null
+++ b/src/ast/normal_forms/CMakeLists.txt
@@ -0,0 +1,11 @@
+z3_add_component(normal_forms
+  SOURCES
+    defined_names.cpp
+    name_exprs.cpp
+    nnf.cpp
+    pull_quant.cpp
+  COMPONENT_DEPENDENCIES
+    rewriter
+  PYG_FILES
+    nnf_params.pyg
+)
diff --git a/src/ast/pattern/CMakeLists.txt b/src/ast/pattern/CMakeLists.txt
new file mode 100644
index 000000000..1f8d43b0b
--- /dev/null
+++ b/src/ast/pattern/CMakeLists.txt
@@ -0,0 +1,36 @@
+# If this code for adding the rule to generate the database file is ever needed
+# for other components then we should refactor this code into
+# z3_add_component()
+if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/database.h")
+  message(FATAL_ERROR "The generated file \"database.h\""
+          ${z3_polluted_tree_msg})
+endif()
+
+add_custom_command(OUTPUT "database.h"
+  COMMAND "${PYTHON_EXECUTABLE}"
+          "${CMAKE_SOURCE_DIR}/scripts/mk_pat_db.py"
+          "${CMAKE_CURRENT_SOURCE_DIR}/database.smt2"
+          "${CMAKE_CURRENT_BINARY_DIR}/database.h"
+  MAIN_DEPENDENCY "${CMAKE_CURRENT_SOURCE_DIR}/database.smt2"
+  DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_pat_db.py"
+          "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+  COMMENT "Generating \"database.h\""
+  USES_TERMINAL
+  VERBATIM
+)
+
+z3_add_component(pattern
+  SOURCES
+    expr_pattern_match.cpp
+    pattern_inference.cpp
+    pattern_inference_params.cpp
+    # Let CMake know this target depends on this generated
+    # header file
+    ${CMAKE_CURRENT_BINARY_DIR}/database.h
+  COMPONENT_DEPENDENCIES
+    normal_forms
+    simplifier
+    smt2parser
+  PYG_FILES
+    pattern_inference_params_helper.pyg
+)
diff --git a/src/ast/proof_checker/CMakeLists.txt b/src/ast/proof_checker/CMakeLists.txt
new file mode 100644
index 000000000..5c947adec
--- /dev/null
+++ b/src/ast/proof_checker/CMakeLists.txt
@@ -0,0 +1,6 @@
+z3_add_component(proof_checker
+  SOURCES
+    proof_checker.cpp
+  COMPONENT_DEPENDENCIES
+    rewriter
+)
diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt
new file mode 100644
index 000000000..59834ea13
--- /dev/null
+++ b/src/ast/rewriter/CMakeLists.txt
@@ -0,0 +1,34 @@
+z3_add_component(rewriter
+  SOURCES
+    arith_rewriter.cpp
+    array_rewriter.cpp
+    ast_counter.cpp
+    bool_rewriter.cpp
+    bv_rewriter.cpp
+    datatype_rewriter.cpp
+    der.cpp
+    dl_rewriter.cpp
+    expr_replacer.cpp
+    expr_safe_replace.cpp
+    factor_rewriter.cpp
+    fpa_rewriter.cpp
+    mk_simplified_app.cpp
+    pb_rewriter.cpp
+    quant_hoist.cpp
+    rewriter.cpp
+    seq_rewriter.cpp
+    th_rewriter.cpp
+    var_subst.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    automata
+    polynomial
+  PYG_FILES
+    arith_rewriter_params.pyg
+    array_rewriter_params.pyg
+    bool_rewriter_params.pyg
+    bv_rewriter_params.pyg
+    fpa_rewriter_params.pyg
+    poly_rewriter_params.pyg
+    rewriter_params.pyg
+)
diff --git a/src/ast/rewriter/bit_blaster/CMakeLists.txt b/src/ast/rewriter/bit_blaster/CMakeLists.txt
new file mode 100644
index 000000000..9eea1558e
--- /dev/null
+++ b/src/ast/rewriter/bit_blaster/CMakeLists.txt
@@ -0,0 +1,8 @@
+z3_add_component(bit_blaster
+  SOURCES
+    bit_blaster.cpp
+    bit_blaster_rewriter.cpp
+  COMPONENT_DEPENDENCIES
+    rewriter
+    simplifier
+)
diff --git a/src/ast/simplifier/CMakeLists.txt b/src/ast/simplifier/CMakeLists.txt
new file mode 100644
index 000000000..7597374a6
--- /dev/null
+++ b/src/ast/simplifier/CMakeLists.txt
@@ -0,0 +1,30 @@
+z3_add_component(simplifier
+  SOURCES
+    arith_simplifier_params.cpp
+    arith_simplifier_plugin.cpp
+    array_simplifier_params.cpp
+    array_simplifier_plugin.cpp
+    basic_simplifier_plugin.cpp
+    bit2int.cpp
+    bv_elim.cpp
+    bv_simplifier_params.cpp
+    bv_simplifier_plugin.cpp
+    datatype_simplifier_plugin.cpp
+    distribute_forall.cpp
+    elim_bounds.cpp
+    fpa_simplifier_plugin.cpp
+    inj_axiom.cpp
+    maximise_ac_sharing.cpp
+    poly_simplifier_plugin.cpp
+    pull_ite_tree.cpp
+    push_app_ite.cpp
+    seq_simplifier_plugin.cpp
+    simplifier.cpp
+    simplifier_plugin.cpp
+  COMPONENT_DEPENDENCIES
+    rewriter
+  PYG_FILES
+    arith_simplifier_params_helper.pyg
+    array_simplifier_params_helper.pyg
+    bv_simplifier_params_helper.pyg
+)
diff --git a/src/ast/substitution/CMakeLists.txt b/src/ast/substitution/CMakeLists.txt
new file mode 100644
index 000000000..80e12c995
--- /dev/null
+++ b/src/ast/substitution/CMakeLists.txt
@@ -0,0 +1,10 @@
+z3_add_component(substitution
+  SOURCES
+    matcher.cpp
+    substitution.cpp
+    substitution_tree.cpp
+    unifier.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    rewriter
+)
diff --git a/src/cmd_context/CMakeLists.txt b/src/cmd_context/CMakeLists.txt
new file mode 100644
index 000000000..8b2d10eec
--- /dev/null
+++ b/src/cmd_context/CMakeLists.txt
@@ -0,0 +1,21 @@
+z3_add_component(cmd_context
+  SOURCES
+    basic_cmds.cpp
+    check_logic.cpp
+    cmd_context.cpp
+    cmd_context_to_goal.cpp
+    cmd_util.cpp
+    context_params.cpp
+    echo_tactic.cpp
+    eval_cmd.cpp
+    interpolant_cmds.cpp
+    parametric_cmd.cpp
+    pdecl.cpp
+    simplify_cmd.cpp
+    tactic_cmds.cpp
+    tactic_manager.cpp
+  COMPONENT_DEPENDENCIES
+    interp
+    rewriter
+    solver
+)
diff --git a/src/cmd_context/extra_cmds/CMakeLists.txt b/src/cmd_context/extra_cmds/CMakeLists.txt
new file mode 100644
index 000000000..3aef1a553
--- /dev/null
+++ b/src/cmd_context/extra_cmds/CMakeLists.txt
@@ -0,0 +1,10 @@
+z3_add_component(extra_cmds
+  SOURCES
+    dbg_cmds.cpp
+    polynomial_cmds.cpp
+    subpaving_cmds.cpp
+  COMPONENT_DEPENDENCIES
+    arith_tactics
+    cmd_context
+    subpaving_tactic
+)
diff --git a/src/duality/CMakeLists.txt b/src/duality/CMakeLists.txt
new file mode 100644
index 000000000..eb2d5c4f2
--- /dev/null
+++ b/src/duality/CMakeLists.txt
@@ -0,0 +1,11 @@
+z3_add_component(duality
+  SOURCES
+    duality_profiling.cpp
+    duality_rpfp.cpp
+    duality_solver.cpp
+    duality_wrapper.cpp
+  COMPONENT_DEPENDENCIES
+    interp
+    qe
+    smt
+)
diff --git a/src/interp/CMakeLists.txt b/src/interp/CMakeLists.txt
new file mode 100644
index 000000000..949811b93
--- /dev/null
+++ b/src/interp/CMakeLists.txt
@@ -0,0 +1,19 @@
+z3_add_component(interp
+  SOURCES
+    iz3base.cpp
+    iz3checker.cpp
+    iz3foci.cpp
+    iz3interp.cpp
+    iz3mgr.cpp
+    iz3pp.cpp
+    iz3profiling.cpp
+    iz3proof.cpp
+    iz3proof_itp.cpp
+    iz3scopes.cpp
+    iz3translate.cpp
+    iz3translate_direct.cpp
+  COMPONENT_DEPENDENCIES
+    solver
+  PYG_FILES
+    interp_params.pyg
+)
diff --git a/src/interp/iz3params.pyg b/src/interp/interp_params.pyg
similarity index 100%
rename from src/interp/iz3params.pyg
rename to src/interp/interp_params.pyg
diff --git a/src/math/automata/CMakeLists.txt b/src/math/automata/CMakeLists.txt
new file mode 100644
index 000000000..1fffd24a8
--- /dev/null
+++ b/src/math/automata/CMakeLists.txt
@@ -0,0 +1,6 @@
+z3_add_component(automata
+  SOURCES
+    automaton.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)
diff --git a/src/math/euclid/CMakeLists.txt b/src/math/euclid/CMakeLists.txt
new file mode 100644
index 000000000..a72f02b28
--- /dev/null
+++ b/src/math/euclid/CMakeLists.txt
@@ -0,0 +1,6 @@
+z3_add_component(euclid
+  SOURCES
+    euclidean_solver.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)
diff --git a/src/math/grobner/CMakeLists.txt b/src/math/grobner/CMakeLists.txt
new file mode 100644
index 000000000..1b56c775f
--- /dev/null
+++ b/src/math/grobner/CMakeLists.txt
@@ -0,0 +1,6 @@
+z3_add_component(grobner
+  SOURCES
+    grobner.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+)
diff --git a/src/math/hilbert/CMakeLists.txt b/src/math/hilbert/CMakeLists.txt
new file mode 100644
index 000000000..2e44140b8
--- /dev/null
+++ b/src/math/hilbert/CMakeLists.txt
@@ -0,0 +1,6 @@
+z3_add_component(hilbert
+  SOURCES
+    hilbert_basis.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)
diff --git a/src/math/interval/CMakeLists.txt b/src/math/interval/CMakeLists.txt
new file mode 100644
index 000000000..390529b9d
--- /dev/null
+++ b/src/math/interval/CMakeLists.txt
@@ -0,0 +1,6 @@
+z3_add_component(interval
+  SOURCES
+    interval_mpq.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)
diff --git a/src/math/polynomial/CMakeLists.txt b/src/math/polynomial/CMakeLists.txt
new file mode 100644
index 000000000..1792f50aa
--- /dev/null
+++ b/src/math/polynomial/CMakeLists.txt
@@ -0,0 +1,16 @@
+z3_add_component(polynomial
+  SOURCES
+    algebraic_numbers.cpp
+    polynomial_cache.cpp
+    polynomial.cpp
+    polynomial_factorization.cpp
+    rpolynomial.cpp
+    sexpr2upolynomial.cpp
+    upolynomial.cpp
+    upolynomial_factorization.cpp
+  COMPONENT_DEPENDENCIES
+    util
+  PYG_FILES
+    algebraic_params.pyg
+)
+
diff --git a/src/math/polynomial/algebraic.pyg b/src/math/polynomial/algebraic_params.pyg
similarity index 100%
rename from src/math/polynomial/algebraic.pyg
rename to src/math/polynomial/algebraic_params.pyg
diff --git a/src/math/realclosure/CMakeLists.txt b/src/math/realclosure/CMakeLists.txt
new file mode 100644
index 000000000..beb5f147b
--- /dev/null
+++ b/src/math/realclosure/CMakeLists.txt
@@ -0,0 +1,9 @@
+z3_add_component(realclosure
+  SOURCES
+    mpz_matrix.cpp
+    realclosure.cpp
+  COMPONENT_DEPENDENCIES
+    interval
+  PYG_FILES
+    rcf_params.pyg
+)
diff --git a/src/math/realclosure/rcf.pyg b/src/math/realclosure/rcf_params.pyg
similarity index 100%
rename from src/math/realclosure/rcf.pyg
rename to src/math/realclosure/rcf_params.pyg
diff --git a/src/math/simplex/CMakeLists.txt b/src/math/simplex/CMakeLists.txt
new file mode 100644
index 000000000..6f965919d
--- /dev/null
+++ b/src/math/simplex/CMakeLists.txt
@@ -0,0 +1,6 @@
+z3_add_component(simplex
+  SOURCES
+    simplex.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)
diff --git a/src/math/subpaving/CMakeLists.txt b/src/math/subpaving/CMakeLists.txt
new file mode 100644
index 000000000..be88f63cd
--- /dev/null
+++ b/src/math/subpaving/CMakeLists.txt
@@ -0,0 +1,11 @@
+z3_add_component(subpaving
+  SOURCES
+    subpaving.cpp
+    subpaving_hwf.cpp
+    subpaving_mpf.cpp
+    subpaving_mpff.cpp
+    subpaving_mpfx.cpp
+    subpaving_mpq.cpp
+  COMPONENT_DEPENDENCIES
+    interval
+)
diff --git a/src/math/subpaving/tactic/CMakeLists.txt b/src/math/subpaving/tactic/CMakeLists.txt
new file mode 100644
index 000000000..eedb0ed4d
--- /dev/null
+++ b/src/math/subpaving/tactic/CMakeLists.txt
@@ -0,0 +1,8 @@
+z3_add_component(subpaving_tactic
+  SOURCES
+    expr2subpaving.cpp
+    subpaving_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    core_tactics
+    subpaving
+)
diff --git a/src/model/CMakeLists.txt b/src/model/CMakeLists.txt
new file mode 100644
index 000000000..0e685e07c
--- /dev/null
+++ b/src/model/CMakeLists.txt
@@ -0,0 +1,18 @@
+z3_add_component(model
+  SOURCES
+    func_interp.cpp
+    model2expr.cpp
+    model_core.cpp
+    model.cpp
+    model_evaluator.cpp
+    model_implicant.cpp
+    model_pp.cpp
+    model_smt2_pp.cpp
+    model_v2_pp.cpp
+  COMPONENT_DEPENDENCIES
+    rewriter
+  PYG_FILES
+    model_evaluator_params.pyg
+    model_params.pyg
+)
+
diff --git a/src/muz/base/CMakeLists.txt b/src/muz/base/CMakeLists.txt
new file mode 100644
index 000000000..ec1ce47c3
--- /dev/null
+++ b/src/muz/base/CMakeLists.txt
@@ -0,0 +1,23 @@
+z3_add_component(muz
+  SOURCES
+    bind_variables.cpp
+    dl_boogie_proof.cpp
+    dl_context.cpp
+    dl_costs.cpp
+    dl_rule.cpp
+    dl_rule_set.cpp
+    dl_rule_subsumption_index.cpp
+    dl_rule_transformer.cpp
+    dl_util.cpp
+    hnf.cpp
+    proof_utils.cpp
+    rule_properties.cpp
+  COMPONENT_DEPENDENCIES
+    aig_tactic
+    qe
+    sat
+    smt
+    smt2parser
+  PYG_FILES
+    fixedpoint_params.pyg
+)
diff --git a/src/muz/bmc/CMakeLists.txt b/src/muz/bmc/CMakeLists.txt
new file mode 100644
index 000000000..dcd99898e
--- /dev/null
+++ b/src/muz/bmc/CMakeLists.txt
@@ -0,0 +1,7 @@
+z3_add_component(bmc
+  SOURCES
+    dl_bmc_engine.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+    transforms
+)
diff --git a/src/muz/clp/CMakeLists.txt b/src/muz/clp/CMakeLists.txt
new file mode 100644
index 000000000..32d9a928e
--- /dev/null
+++ b/src/muz/clp/CMakeLists.txt
@@ -0,0 +1,7 @@
+z3_add_component(clp
+  SOURCES
+    clp_context.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+    transforms
+)
diff --git a/src/muz/dataflow/CMakeLists.txt b/src/muz/dataflow/CMakeLists.txt
new file mode 100644
index 000000000..3fc1e1f19
--- /dev/null
+++ b/src/muz/dataflow/CMakeLists.txt
@@ -0,0 +1,6 @@
+z3_add_component(dataflow
+  SOURCES
+    dataflow.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+)
diff --git a/src/muz/ddnf/CMakeLists.txt b/src/muz/ddnf/CMakeLists.txt
new file mode 100644
index 000000000..55d6bae5d
--- /dev/null
+++ b/src/muz/ddnf/CMakeLists.txt
@@ -0,0 +1,8 @@
+z3_add_component(ddnf
+  SOURCES
+    ddnf.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+    rel
+    transforms
+)
diff --git a/src/muz/duality/CMakeLists.txt b/src/muz/duality/CMakeLists.txt
new file mode 100644
index 000000000..f005b88b1
--- /dev/null
+++ b/src/muz/duality/CMakeLists.txt
@@ -0,0 +1,8 @@
+z3_add_component(duality_intf
+  SOURCES
+    duality_dl_interface.cpp
+  COMPONENT_DEPENDENCIES
+    duality
+    muz
+    transforms
+)
diff --git a/src/muz/fp/CMakeLists.txt b/src/muz/fp/CMakeLists.txt
new file mode 100644
index 000000000..239c4df12
--- /dev/null
+++ b/src/muz/fp/CMakeLists.txt
@@ -0,0 +1,16 @@
+z3_add_component(fp
+  SOURCES
+    datalog_parser.cpp
+    dl_cmds.cpp
+    dl_register_engine.cpp
+    horn_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    bmc
+    clp
+    ddnf
+    duality_intf
+    muz
+    pdr
+    rel
+    tab
+)
diff --git a/src/muz/pdr/CMakeLists.txt b/src/muz/pdr/CMakeLists.txt
new file mode 100644
index 000000000..ca2992b97
--- /dev/null
+++ b/src/muz/pdr/CMakeLists.txt
@@ -0,0 +1,20 @@
+z3_add_component(pdr
+  SOURCES
+    pdr_closure.cpp
+    pdr_context.cpp
+    pdr_dl_interface.cpp
+    pdr_farkas_learner.cpp
+    pdr_generalizers.cpp
+    pdr_manager.cpp
+    pdr_prop_solver.cpp
+    pdr_reachable_cache.cpp
+    pdr_smt_context_manager.cpp
+    pdr_sym_mux.cpp
+    pdr_util.cpp
+  COMPONENT_DEPENDENCIES
+    arith_tactics
+    core_tactics
+    muz
+    smt_tactic
+    transforms
+)
diff --git a/src/muz/rel/CMakeLists.txt b/src/muz/rel/CMakeLists.txt
new file mode 100644
index 000000000..720714ed8
--- /dev/null
+++ b/src/muz/rel/CMakeLists.txt
@@ -0,0 +1,32 @@
+z3_add_component(rel
+  SOURCES
+    aig_exporter.cpp
+    check_relation.cpp
+    dl_base.cpp
+    dl_bound_relation.cpp
+    dl_check_table.cpp
+    dl_compiler.cpp
+    dl_external_relation.cpp
+    dl_finite_product_relation.cpp
+    dl_instruction.cpp
+    dl_interval_relation.cpp
+    dl_lazy_table.cpp
+    dl_mk_explanations.cpp
+    dl_mk_partial_equiv.cpp
+    dl_mk_similarity_compressor.cpp
+    dl_mk_simple_joins.cpp
+    dl_product_relation.cpp
+    dl_relation_manager.cpp
+    dl_sieve_relation.cpp
+    dl_sparse_table.cpp
+    dl_table.cpp
+    dl_table_relation.cpp
+    doc.cpp
+    karr_relation.cpp
+    rel_context.cpp
+    tbv.cpp
+    udoc_relation.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+    transforms
+)
diff --git a/src/muz/tab/CMakeLists.txt b/src/muz/tab/CMakeLists.txt
new file mode 100644
index 000000000..cfae51280
--- /dev/null
+++ b/src/muz/tab/CMakeLists.txt
@@ -0,0 +1,7 @@
+z3_add_component(tab
+  SOURCES
+    tab_context.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+    transforms
+)
diff --git a/src/muz/transforms/CMakeLists.txt b/src/muz/transforms/CMakeLists.txt
new file mode 100644
index 000000000..6a0a1ac9c
--- /dev/null
+++ b/src/muz/transforms/CMakeLists.txt
@@ -0,0 +1,28 @@
+z3_add_component(transforms
+  SOURCES
+    dl_mk_array_blast.cpp
+    dl_mk_backwards.cpp
+    dl_mk_bit_blast.cpp
+    dl_mk_coalesce.cpp
+    dl_mk_coi_filter.cpp
+    dl_mk_filter_rules.cpp
+    dl_mk_interp_tail_simplifier.cpp
+    dl_mk_karr_invariants.cpp
+    dl_mk_loop_counter.cpp
+    dl_mk_magic_sets.cpp
+    dl_mk_magic_symbolic.cpp
+    dl_mk_quantifier_abstraction.cpp
+    dl_mk_quantifier_instantiation.cpp
+    dl_mk_rule_inliner.cpp
+    dl_mk_scale.cpp
+    dl_mk_separate_negated_tails.cpp
+    dl_mk_slice.cpp
+    dl_mk_subsumption_checker.cpp
+    dl_mk_unbound_compressor.cpp
+    dl_mk_unfold.cpp
+    dl_transforms.cpp
+  COMPONENT_DEPENDENCIES
+    dataflow
+    hilbert
+    muz
+)
diff --git a/src/nlsat/CMakeLists.txt b/src/nlsat/CMakeLists.txt
new file mode 100644
index 000000000..d0c1379e5
--- /dev/null
+++ b/src/nlsat/CMakeLists.txt
@@ -0,0 +1,14 @@
+z3_add_component(nlsat
+  SOURCES
+    nlsat_clause.cpp
+    nlsat_evaluator.cpp
+    nlsat_explain.cpp
+    nlsat_interval_set.cpp
+    nlsat_solver.cpp
+    nlsat_types.cpp
+  COMPONENT_DEPENDENCIES
+    polynomial
+    sat
+  PYG_FILES
+    nlsat_params.pyg
+)
diff --git a/src/nlsat/tactic/CMakeLists.txt b/src/nlsat/tactic/CMakeLists.txt
new file mode 100644
index 000000000..9ea26a0c5
--- /dev/null
+++ b/src/nlsat/tactic/CMakeLists.txt
@@ -0,0 +1,10 @@
+z3_add_component(nlsat_tactic
+  SOURCES
+    goal2nlsat.cpp
+    nlsat_tactic.cpp
+    qfnra_nlsat_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    arith_tactics
+    nlsat
+    sat_tactic
+)
diff --git a/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt
new file mode 100644
index 000000000..c50f8be52
--- /dev/null
+++ b/src/opt/CMakeLists.txt
@@ -0,0 +1,26 @@
+z3_add_component(opt
+  SOURCES
+    bcd2.cpp
+    fu_malik.cpp
+    hitting_sets.cpp
+    maxhs.cpp
+    maxres.cpp
+    maxsls.cpp
+    maxsmt.cpp
+    mss.cpp
+    mus.cpp
+    opt_cmds.cpp
+    opt_context.cpp
+    opt_pareto.cpp
+    optsmt.cpp
+    opt_solver.cpp
+    pb_sls.cpp
+    wmax.cpp
+  COMPONENT_DEPENDENCIES
+    sat_solver
+    sls_tactic
+    smt
+    smtlogic_tactics
+  PYG_FILES
+    opt_params.pyg
+)
diff --git a/src/parsers/smt/CMakeLists.txt b/src/parsers/smt/CMakeLists.txt
new file mode 100644
index 000000000..2edf7b679
--- /dev/null
+++ b/src/parsers/smt/CMakeLists.txt
@@ -0,0 +1,8 @@
+z3_add_component(smtparser
+  SOURCES
+    smtlib.cpp
+    smtlib_solver.cpp
+    smtparser.cpp
+  COMPONENT_DEPENDENCIES
+    portfolio
+)
diff --git a/src/parsers/smt2/CMakeLists.txt b/src/parsers/smt2/CMakeLists.txt
new file mode 100644
index 000000000..1467d95c6
--- /dev/null
+++ b/src/parsers/smt2/CMakeLists.txt
@@ -0,0 +1,8 @@
+z3_add_component(smt2parser
+  SOURCES
+    smt2parser.cpp
+    smt2scanner.cpp
+  COMPONENT_DEPENDENCIES
+    cmd_context
+    parser_util
+)
diff --git a/src/parsers/util/CMakeLists.txt b/src/parsers/util/CMakeLists.txt
new file mode 100644
index 000000000..6ede4b773
--- /dev/null
+++ b/src/parsers/util/CMakeLists.txt
@@ -0,0 +1,11 @@
+z3_add_component(parser_util
+  SOURCES
+    cost_parser.cpp
+    pattern_validation.cpp
+    scanner.cpp
+    simple_parser.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+  PYG_FILES
+    parser_params.pyg
+)
diff --git a/src/qe/CMakeLists.txt b/src/qe/CMakeLists.txt
new file mode 100644
index 000000000..9db253bd6
--- /dev/null
+++ b/src/qe/CMakeLists.txt
@@ -0,0 +1,21 @@
+z3_add_component(qe
+  SOURCES
+    nlarith_util.cpp
+    qe_arith.cpp
+    qe_arith_plugin.cpp
+    qe_array_plugin.cpp
+    qe_bool_plugin.cpp
+    qe_bv_plugin.cpp
+    qe_cmd.cpp
+    qe.cpp
+    qe_datatype_plugin.cpp
+    qe_dl_plugin.cpp
+    qe_lite.cpp
+    qe_sat_tactic.cpp
+    qe_tactic.cpp
+    qe_util.cpp
+    vsubst_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    sat
+    smt
+)
diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt
new file mode 100644
index 000000000..cfc3835c1
--- /dev/null
+++ b/src/sat/CMakeLists.txt
@@ -0,0 +1,29 @@
+z3_add_component(sat
+  SOURCES
+    dimacs.cpp
+    sat_asymm_branch.cpp
+    sat_bceq.cpp
+    sat_clause.cpp
+    sat_clause_set.cpp
+    sat_clause_use_list.cpp
+    sat_cleaner.cpp
+    sat_config.cpp
+    sat_elim_eqs.cpp
+    sat_iff3_finder.cpp
+    sat_integrity_checker.cpp
+    sat_model_converter.cpp
+    sat_mus.cpp
+    sat_probing.cpp
+    sat_scc.cpp
+    sat_simplifier.cpp
+    sat_sls.cpp
+    sat_solver.cpp
+    sat_watched.cpp
+  COMPONENT_DEPENDENCIES
+    util
+  PYG_FILES
+    sat_asymm_branch_params.pyg
+    sat_params.pyg
+    sat_scc_params.pyg
+    sat_simplifier_params.pyg
+)
diff --git a/src/sat/sat_solver/CMakeLists.txt b/src/sat/sat_solver/CMakeLists.txt
new file mode 100644
index 000000000..14eb4ac25
--- /dev/null
+++ b/src/sat/sat_solver/CMakeLists.txt
@@ -0,0 +1,11 @@
+z3_add_component(sat_solver
+  SOURCES
+    inc_sat_solver.cpp
+  COMPONENT_DEPENDENCIES
+    aig_tactic
+    arith_tactics
+    bv_tactics
+    core_tactics
+    sat_tactic
+    solver
+)
diff --git a/src/sat/tactic/CMakeLists.txt b/src/sat/tactic/CMakeLists.txt
new file mode 100644
index 000000000..74aeba8b9
--- /dev/null
+++ b/src/sat/tactic/CMakeLists.txt
@@ -0,0 +1,9 @@
+z3_add_component(sat_tactic
+  SOURCES
+    atom2bool_var.cpp
+    goal2sat.cpp
+    sat_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    sat
+    tactic
+)
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
new file mode 100644
index 000000000..82113bbb7
--- /dev/null
+++ b/src/shell/CMakeLists.txt
@@ -0,0 +1,47 @@
+set (shell_object_files "")
+# FIXME: z3 should really link against libz3 and not the
+# individual components. Several things prevent us from
+# doing this
+# * The api_dll component in libz3 shouldn't be used the
+#   the z3 executable.
+# * The z3 executable uses symbols that are hidden in libz3
+
+# We are only using these dependencies to enforce a build
+# order. We don't use this list for actual linking.
+set(shell_deps api extra_cmds opt sat)
+z3_expand_dependencies(shell_expanded_deps ${shell_deps})
+get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS)
+foreach (component ${Z3_LIBZ3_COMPONENTS_LIST})
+  if ("${component}" STREQUAL "api_dll")
+    # We don't use the api_dll component in the Z3 executable
+    continue()
+  endif()
+  list(APPEND shell_object_files $<TARGET_OBJECTS:${component}>)
+endforeach()
+add_executable(shell
+  datalog_frontend.cpp
+  dimacs_frontend.cpp
+  "${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp"
+  "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp"
+  main.cpp
+  "${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp"
+  opt_frontend.cpp
+  smtlib_frontend.cpp
+  z3_log_frontend.cpp
+# FIXME: shell should really link against libz3 but it can't due to requiring
+# use of some hidden symbols. Also libz3 has the ``api_dll`` component which
+# we don't want (I think).
+  ${shell_object_files}
+)
+z3_add_install_tactic_rule(${shell_deps})
+z3_add_memory_initializer_rule(${shell_deps})
+z3_add_gparams_register_modules_rule(${shell_deps})
+set_target_properties(shell PROPERTIES OUTPUT_NAME z3)
+target_compile_definitions(shell PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
+target_compile_options(shell PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
+target_include_directories(shell PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
+target_link_libraries(shell PRIVATE ${Z3_DEPENDENT_LIBS})
+z3_add_component_dependencies_to_target(shell ${shell_expanded_deps})
+install(TARGETS shell
+  RUNTIME DESTINATION "${Z3_INSTALL_BIN_DIR}"
+)
diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
new file mode 100644
index 000000000..e9306b2d6
--- /dev/null
+++ b/src/smt/CMakeLists.txt
@@ -0,0 +1,77 @@
+z3_add_component(smt
+  SOURCES
+    arith_eq_adapter.cpp
+    arith_eq_solver.cpp
+    asserted_formulas.cpp
+    cached_var_subst.cpp
+    cost_evaluator.cpp
+    dyn_ack.cpp
+    elim_term_ite.cpp
+    expr_context_simplifier.cpp
+    fingerprints.cpp
+    mam.cpp
+    old_interval.cpp
+    qi_queue.cpp
+    smt_almost_cg_table.cpp
+    smt_case_split_queue.cpp
+    smt_cg_table.cpp
+    smt_checker.cpp
+    smt_clause.cpp
+    smt_conflict_resolution.cpp
+    smt_context.cpp
+    smt_context_inv.cpp
+    smt_context_pp.cpp
+    smt_context_stat.cpp
+    smt_enode.cpp
+    smt_farkas_util.cpp
+    smt_for_each_relevant_expr.cpp
+    smt_implied_equalities.cpp
+    smt_internalizer.cpp
+    smt_justification.cpp
+    smt_kernel.cpp
+    smt_literal.cpp
+    smt_model_checker.cpp
+    smt_model_finder.cpp
+    smt_model_generator.cpp
+    smt_quantifier.cpp
+    smt_quantifier_stat.cpp
+    smt_quick_checker.cpp
+    smt_relevancy.cpp
+    smt_setup.cpp
+    smt_solver.cpp
+    smt_statistics.cpp
+    smt_theory.cpp
+    smt_value_sort.cpp
+    theory_arith.cpp
+    theory_array_base.cpp
+    theory_array.cpp
+    theory_array_full.cpp
+    theory_bv.cpp
+    theory_datatype.cpp
+    theory_dense_diff_logic.cpp
+    theory_diff_logic.cpp
+    theory_dl.cpp
+    theory_dummy.cpp
+    theory_fpa.cpp
+    theory_opt.cpp
+    theory_pb.cpp
+    theory_seq.cpp
+    theory_utvpi.cpp
+    theory_wmaxsat.cpp
+    uses_theory.cpp
+    watch_list.cpp
+  COMPONENT_DEPENDENCIES
+    bit_blaster
+    cmd_context
+    euclid
+    fpa
+    grobner
+    macros
+    normal_forms
+    parser_util
+    pattern
+    proof_checker
+    proto_model
+    simplex
+    substitution
+)
diff --git a/src/smt/params/CMakeLists.txt b/src/smt/params/CMakeLists.txt
new file mode 100644
index 000000000..67224a287
--- /dev/null
+++ b/src/smt/params/CMakeLists.txt
@@ -0,0 +1,18 @@
+z3_add_component(smt_params
+  SOURCES
+    dyn_ack_params.cpp
+    preprocessor_params.cpp
+    qi_params.cpp
+    smt_params.cpp
+    theory_arith_params.cpp
+    theory_array_params.cpp
+    theory_bv_params.cpp
+    theory_pb_params.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    bit_blaster
+    pattern
+    simplifier
+  PYG_FILES
+    smt_params_helper.pyg
+)
diff --git a/src/smt/proto_model/CMakeLists.txt b/src/smt/proto_model/CMakeLists.txt
new file mode 100644
index 000000000..0539c0fb0
--- /dev/null
+++ b/src/smt/proto_model/CMakeLists.txt
@@ -0,0 +1,13 @@
+z3_add_component(proto_model
+  SOURCES
+    array_factory.cpp
+    datatype_factory.cpp
+    numeral_factory.cpp
+    proto_model.cpp
+    struct_factory.cpp
+    value_factory.cpp
+  COMPONENT_DEPENDENCIES
+    model
+    simplifier
+    smt_params
+)
diff --git a/src/smt/tactic/CMakeLists.txt b/src/smt/tactic/CMakeLists.txt
new file mode 100644
index 000000000..b7525bda8
--- /dev/null
+++ b/src/smt/tactic/CMakeLists.txt
@@ -0,0 +1,8 @@
+z3_add_component(smt_tactic
+  SOURCES
+    ctx_solver_simplify_tactic.cpp
+    smt_tactic.cpp
+    unit_subsumption_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    smt
+)
diff --git a/src/solver/CMakeLists.txt b/src/solver/CMakeLists.txt
new file mode 100644
index 000000000..5e76c91ce
--- /dev/null
+++ b/src/solver/CMakeLists.txt
@@ -0,0 +1,13 @@
+z3_add_component(solver
+  SOURCES
+    check_sat_result.cpp
+    combined_solver.cpp
+    solver.cpp
+    solver_na2as.cpp
+    tactic2solver.cpp
+  COMPONENT_DEPENDENCIES
+    model
+    tactic
+  PYG_FILES
+    combined_solver_params.pyg
+)
diff --git a/src/tactic/CMakeLists.txt b/src/tactic/CMakeLists.txt
new file mode 100644
index 000000000..318803cd2
--- /dev/null
+++ b/src/tactic/CMakeLists.txt
@@ -0,0 +1,20 @@
+z3_add_component(tactic
+  SOURCES
+    equiv_proof_converter.cpp
+    extension_model_converter.cpp
+    filter_model_converter.cpp
+    goal.cpp
+    goal_num_occurs.cpp
+    goal_shared_occs.cpp
+    goal_util.cpp
+    horn_subsume_model_converter.cpp
+    model_converter.cpp
+    probe.cpp
+    proof_converter.cpp
+    replace_proof_converter.cpp
+    tactical.cpp
+    tactic.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    model
+)
diff --git a/src/tactic/aig/CMakeLists.txt b/src/tactic/aig/CMakeLists.txt
new file mode 100644
index 000000000..1e1a0d266
--- /dev/null
+++ b/src/tactic/aig/CMakeLists.txt
@@ -0,0 +1,7 @@
+z3_add_component(aig_tactic
+  SOURCES
+    aig.cpp
+    aig_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    tactic
+)
diff --git a/src/tactic/arith/CMakeLists.txt b/src/tactic/arith/CMakeLists.txt
new file mode 100644
index 000000000..cdc42367a
--- /dev/null
+++ b/src/tactic/arith/CMakeLists.txt
@@ -0,0 +1,31 @@
+z3_add_component(arith_tactics
+  SOURCES
+    add_bounds_tactic.cpp
+    arith_bounds_tactic.cpp
+    bound_manager.cpp
+    bound_propagator.cpp
+    bv2int_rewriter.cpp
+    bv2real_rewriter.cpp
+    card2bv_tactic.cpp
+    degree_shift_tactic.cpp
+    diff_neq_tactic.cpp
+    elim01_tactic.cpp
+    eq2bv_tactic.cpp
+    factor_tactic.cpp
+    fix_dl_var_tactic.cpp
+    fm_tactic.cpp
+    lia2card_tactic.cpp
+    lia2pb_tactic.cpp
+    linear_equation.cpp
+    nla2bv_tactic.cpp
+    normalize_bounds_tactic.cpp
+    pb2bv_model_converter.cpp
+    pb2bv_tactic.cpp
+    probe_arith.cpp
+    propagate_ineqs_tactic.cpp
+    purify_arith_tactic.cpp
+    recover_01_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    core_tactics
+    sat
+)
diff --git a/src/tactic/bv/CMakeLists.txt b/src/tactic/bv/CMakeLists.txt
new file mode 100644
index 000000000..42cff2bfc
--- /dev/null
+++ b/src/tactic/bv/CMakeLists.txt
@@ -0,0 +1,16 @@
+z3_add_component(bv_tactics
+  SOURCES
+    bit_blaster_model_converter.cpp
+    bit_blaster_tactic.cpp
+    bv1_blaster_tactic.cpp
+    bvarray2uf_rewriter.cpp
+    bvarray2uf_tactic.cpp
+    bv_bounds_tactic.cpp
+    bv_size_reduction_tactic.cpp
+    elim_small_bv_tactic.cpp
+    max_bv_sharing_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    bit_blaster
+    core_tactics
+    tactic
+)
diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt
new file mode 100644
index 000000000..d59265c5c
--- /dev/null
+++ b/src/tactic/core/CMakeLists.txt
@@ -0,0 +1,25 @@
+z3_add_component(core_tactics
+  SOURCES
+    blast_term_ite_tactic.cpp
+    cofactor_elim_term_ite.cpp
+    cofactor_term_ite_tactic.cpp
+    ctx_simplify_tactic.cpp
+    der_tactic.cpp
+    distribute_forall_tactic.cpp
+    elim_term_ite_tactic.cpp
+    elim_uncnstr_tactic.cpp
+    nnf_tactic.cpp
+    occf_tactic.cpp
+    pb_preprocess_tactic.cpp
+    propagate_values_tactic.cpp
+    reduce_args_tactic.cpp
+    simplify_tactic.cpp
+    solve_eqs_tactic.cpp
+    split_clause_tactic.cpp
+    symmetry_reduce_tactic.cpp
+    tseitin_cnf_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    normal_forms
+    tactic
+)
+
diff --git a/src/tactic/fpa/CMakeLists.txt b/src/tactic/fpa/CMakeLists.txt
new file mode 100644
index 000000000..d93cd5b82
--- /dev/null
+++ b/src/tactic/fpa/CMakeLists.txt
@@ -0,0 +1,14 @@
+z3_add_component(fpa_tactics
+  SOURCES
+    fpa2bv_model_converter.cpp
+    fpa2bv_tactic.cpp
+    qffp_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    arith_tactics
+    bv_tactics
+    core_tactics
+    fpa
+    sat_tactic
+    smtlogic_tactics
+    smt_tactic
+)
diff --git a/src/tactic/nlsat_smt/CMakeLists.txt b/src/tactic/nlsat_smt/CMakeLists.txt
new file mode 100644
index 000000000..e28b11966
--- /dev/null
+++ b/src/tactic/nlsat_smt/CMakeLists.txt
@@ -0,0 +1,7 @@
+z3_add_component(nlsat_smt_tactic
+  SOURCES
+    nl_purify_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    nlsat_tactic
+    smt_tactic
+)
diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt
new file mode 100644
index 000000000..d20af772b
--- /dev/null
+++ b/src/tactic/portfolio/CMakeLists.txt
@@ -0,0 +1,15 @@
+z3_add_component(portfolio
+  SOURCES
+    default_tactic.cpp
+    smt_strategic_solver.cpp
+  COMPONENT_DEPENDENCIES
+    aig_tactic
+    fp
+    fpa_tactics
+    qe
+    sat_solver
+    sls_tactic
+    smtlogic_tactics
+    subpaving_tactic
+    ufbv_tactic
+)
diff --git a/src/tactic/sls/CMakeLists.txt b/src/tactic/sls/CMakeLists.txt
new file mode 100644
index 000000000..8b720b333
--- /dev/null
+++ b/src/tactic/sls/CMakeLists.txt
@@ -0,0 +1,13 @@
+z3_add_component(sls_tactic
+  SOURCES
+    bvsls_opt_engine.cpp
+    sls_engine.cpp
+    sls_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    bv_tactics
+    core_tactics
+    normal_forms
+    tactic
+  PYG_FILES
+    sls_params.pyg
+)
diff --git a/src/tactic/smtlogics/CMakeLists.txt b/src/tactic/smtlogics/CMakeLists.txt
new file mode 100644
index 000000000..840dd008a
--- /dev/null
+++ b/src/tactic/smtlogics/CMakeLists.txt
@@ -0,0 +1,31 @@
+z3_add_component(smtlogic_tactics
+  SOURCES
+    nra_tactic.cpp
+    qfaufbv_tactic.cpp
+    qfauflia_tactic.cpp
+    qfbv_tactic.cpp
+    qfidl_tactic.cpp
+    qflia_tactic.cpp
+    qflra_tactic.cpp
+    qfnia_tactic.cpp
+    qfnra_tactic.cpp
+    qfufbv_ackr_model_converter.cpp
+    qfufbv_tactic.cpp
+    qfufnra_tactic.cpp
+    qfuf_tactic.cpp
+    quant_tactics.cpp
+  COMPONENT_DEPENDENCIES
+    ackermannization
+    aig_tactic
+    arith_tactics
+    bv_tactics
+    fp
+    muz
+    nlsat_tactic
+    nlsat_smt_tactic
+    qe
+    sat_solver
+    smt_tactic
+  PYG_FILES
+    qfufbv_tactic_params.pyg
+)
diff --git a/src/tactic/ufbv/CMakeLists.txt b/src/tactic/ufbv/CMakeLists.txt
new file mode 100644
index 000000000..c1d6daaaa
--- /dev/null
+++ b/src/tactic/ufbv/CMakeLists.txt
@@ -0,0 +1,14 @@
+z3_add_component(ufbv_tactic
+  SOURCES
+    macro_finder_tactic.cpp
+    quasi_macros_tactic.cpp
+    ufbv_rewriter.cpp
+    ufbv_rewriter_tactic.cpp
+    ufbv_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    core_tactics
+    macros
+    normal_forms
+    rewriter
+    smt_tactic
+)
diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
new file mode 100644
index 000000000..0217e99b6
--- /dev/null
+++ b/src/test/CMakeLists.txt
@@ -0,0 +1,125 @@
+add_subdirectory(fuzzing)
+################################################################################
+# z3-test executable
+################################################################################
+set(z3_test_deps api fuzzing simplex)
+z3_expand_dependencies(z3_test_expanded_deps ${z3_test_deps})
+set (z3_test_extra_object_files "")
+foreach (component ${z3_test_expanded_deps})
+  list(APPEND z3_test_extra_object_files $<TARGET_OBJECTS:${component}>)
+endforeach()
+add_executable(test-z3
+  EXCLUDE_FROM_ALL
+  algebraic.cpp
+  api_bug.cpp
+  api.cpp
+  arith_rewriter.cpp
+  arith_simplifier_plugin.cpp
+  ast.cpp
+  bit_blaster.cpp
+  bits.cpp
+  bit_vector.cpp
+  buffer.cpp
+  bv_simplifier_plugin.cpp
+  chashtable.cpp
+  check_assumptions.cpp
+  datalog_parser.cpp
+  ddnf.cpp
+  diff_logic.cpp
+  dl_context.cpp
+  dl_product_relation.cpp
+  dl_query.cpp
+  dl_relation.cpp
+  dl_table.cpp
+  dl_util.cpp
+  doc.cpp
+  escaped.cpp
+  ex.cpp
+  expr_rand.cpp
+  expr_substitution.cpp
+  ext_numeral.cpp
+  f2n.cpp
+  factor_rewriter.cpp
+  fixed_bit_vector.cpp
+  for_each_file.cpp
+  get_implied_equalities.cpp
+  "${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp"
+  hashtable.cpp
+  heap.cpp
+  heap_trie.cpp
+  hilbert_basis.cpp
+  horn_subsume_model_converter.cpp
+  hwf.cpp
+  inf_rational.cpp
+  "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp"
+  interval.cpp
+  karr.cpp
+  list.cpp
+  main.cpp
+  map.cpp
+  matcher.cpp
+  "${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp"
+  memory.cpp
+  model2expr.cpp
+  model_retrieval.cpp
+  mpbq.cpp
+  mpf.cpp
+  mpff.cpp
+  mpfx.cpp
+  mpq.cpp
+  mpz.cpp
+  nlarith_util.cpp
+  nlsat.cpp
+  no_overflow.cpp
+  object_allocator.cpp
+  old_interval.cpp
+  optional.cpp
+  parray.cpp
+  pdr.cpp
+  permutation.cpp
+  polynomial.cpp
+  polynomial_factorization.cpp
+  polynorm.cpp
+  prime_generator.cpp
+  proof_checker.cpp
+  qe_arith.cpp
+  quant_elim.cpp
+  quant_solve.cpp
+  random.cpp
+  rational.cpp
+  rcf.cpp
+  region.cpp
+  sat_user_scope.cpp
+  simple_parser.cpp
+  simplex.cpp
+  simplifier.cpp
+  small_object_allocator.cpp
+  smt2print_parse.cpp
+  smt_context.cpp
+  sorting_network.cpp
+  stack.cpp
+  string_buffer.cpp
+  substitution.cpp
+  symbol.cpp
+  symbol_table.cpp
+  tbv.cpp
+  theory_dl.cpp
+  theory_pb.cpp
+  timeout.cpp
+  total_order.cpp
+  trigo.cpp
+  udoc_relation.cpp
+  uint_set.cpp
+  upolynomial.cpp
+  var_subst.cpp
+  vector.cpp
+  ${z3_test_extra_object_files}
+)
+z3_add_install_tactic_rule(${z3_test_deps})
+z3_add_memory_initializer_rule(${z3_test_deps})
+z3_add_gparams_register_modules_rule(${z3_test_deps})
+target_compile_definitions(test-z3 PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
+target_compile_options(test-z3 PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
+target_link_libraries(test-z3 PRIVATE ${Z3_DEPENDENT_LIBS})
+target_include_directories(shell PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
+z3_add_component_dependencies_to_target(test-z3 ${z3_test_expanded_deps})
diff --git a/src/test/fuzzing/CMakeLists.txt b/src/test/fuzzing/CMakeLists.txt
new file mode 100644
index 000000000..c2bc61ed5
--- /dev/null
+++ b/src/test/fuzzing/CMakeLists.txt
@@ -0,0 +1,8 @@
+z3_add_component(fuzzing
+  NOT_LIBZ3_COMPONENT # Don't put this component inside libz3
+  SOURCES
+    expr_delta.cpp
+    expr_rand.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+)
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
new file mode 100644
index 000000000..c85076531
--- /dev/null
+++ b/src/util/CMakeLists.txt
@@ -0,0 +1,60 @@
+if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/version.h")
+  message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/version.h\""
+          ${z3_polluted_tree_msg}
+  )
+endif()
+configure_file(version.h.in ${CMAKE_CURRENT_BINARY_DIR}/version.h @ONLY)
+
+z3_add_component(util
+  SOURCES
+    approx_nat.cpp
+    approx_set.cpp
+    bit_util.cpp
+    bit_vector.cpp
+    cmd_context_types.cpp
+    common_msgs.cpp
+    cooperate.cpp
+    debug.cpp
+    env_params.cpp
+    fixed_bit_vector.cpp
+    gparams.cpp
+    hash.cpp
+    hwf.cpp
+    inf_int_rational.cpp
+    inf_rational.cpp
+    inf_s_integer.cpp
+    lbool.cpp
+    luby.cpp
+    memory_manager.cpp
+    mpbq.cpp
+    mpf.cpp
+    mpff.cpp
+    mpfx.cpp
+    mpn.cpp
+    mpq.cpp
+    mpq_inf.cpp
+    mpz.cpp
+    page.cpp
+    params.cpp
+    permutation.cpp
+    prime_generator.cpp
+    rational.cpp
+    region.cpp
+    rlimit.cpp
+    scoped_ctrl_c.cpp
+    scoped_timer.cpp
+    sexpr.cpp
+    s_integer.cpp
+    small_object_allocator.cpp
+    smt2_util.cpp
+    stack.cpp
+    statistics.cpp
+    symbol.cpp
+    timeit.cpp
+    timeout.cpp
+    timer.cpp
+    trace.cpp
+    util.cpp
+    warning.cpp
+    z3_exception.cpp
+)
diff --git a/src/util/version.h.in b/src/util/version.h.in
new file mode 100644
index 000000000..05b619f2d
--- /dev/null
+++ b/src/util/version.h.in
@@ -0,0 +1,5 @@
+// automatically generated file.
+#define Z3_MAJOR_VERSION   @Z3_VERSION_MAJOR@
+#define Z3_MINOR_VERSION   @Z3_VERSION_MINOR@
+#define Z3_BUILD_NUMBER    @Z3_VERSION_PATCH@
+#define Z3_REVISION_NUMBER @Z3_VERSION_TWEAK@