diff --git a/README-CMake.md b/README-CMake.md
index a7b96c659..cbdcbd158 100644
--- a/README-CMake.md
+++ b/README-CMake.md
@@ -10,39 +10,56 @@ on your platform. Example generators include "UNIX Makfiles" and "Visual Studio
 
 ## Getting started
 
-The general workflow when using CMake is the following
+### Fixing a polluted source tree
 
-1. Create a new build directory
-2. Configure the project
-3. Generate the build system
-4. Invoke the build system to build the project
+If you have never used the python build system you can skip this step.
 
-To perform steps 2 and 3 you can choose from three different tools
+The existing Python build system creates generated source files in
+the build tree. The CMake build system will refuse to work if it
+detects this so you need to clean your build tree first.
 
-* cmake
-* ccmake
-* cmake-gui
+To do this run the following in the root of the repository
 
-``cmake`` is a command line tool and is what you should use if you are
-writing a script to build Z3. This tool performs steps 1 and 2 in one
-go without user interaction. The ``ccmake`` and ``cmake-gui`` tools are
-more interactive and allow you to change various options. In both these
-tools the basic steps to follow are:
+```
+git clean -nx src
+```
 
-1. Configure.
-2. Change any options you wish. Everytime you change a set of options
-   You should configure again. This may cause new options to appear
-3. Generate.
+This will list everything that will be removed. If you are happy
+with this then run.
 
-For information see https://cmake.org/runningcmake/
+```
+git clean -fx src
+```
 
-Note when invoking CMake you give it the path to the source directory.
-This is the top-level directory in the Z3 repository containing a
-``CMakeLists.txt``. That file should contain the line ``project(Z3 C CXX)``.
-If you give it a path deeper into the Z3 repository (e.g. the ``src`` directory)
-the configure step will fail.
+which will remove the generated source files.
 
-What follows is a brief walk through of how to build Z3 using various generators.
+### Bootstrapping
+
+Most of Z3's CMake files do not live in their correct location. Instead those
+files live in the ``contrib/cmake`` folder and a script is provided that will
+copy (or hard link) the files into their correct location.
+
+To copy the files run
+
+```
+python contrib/cmake/bootstrap.py create
+```
+
+in the root of the repository. Once you have done this you can now build Z3 using CMake.
+Remember to rerun this command if you pull down new code or change branch so
+that the CMake files are up to date.
+
+To remove the copied files run
+
+```
+python contrib/cmake/bootstrap.py remove
+```
+
+Note if you plan to do development on Z3 you should read the developer
+notes on bootstrapping in this document.
+
+What follows is a brief walk through of how to build Z3 using some
+of the more commonly used CMake generators.
 
 ### Unix Makefiles
 
@@ -52,7 +69,7 @@ Run the following in the top level directory of the Z3 repository.
 mkdir build
 cd build
 cmake -G "Unix Makefiles" ../
-make -j4
+make -j4 # Replace 4 with an appropriate number
 ```
 
 Note that on some platforms "Unix Makesfiles" is the default generator so on those
@@ -131,7 +148,7 @@ environment where the compiler can be found. If you have Visual Studio
 installed it typically ships with a "Developer Command Prompt Window" that you
 can use which has the environment variables setup for you.
 
-## NMake
+### NMake
 
 NMake is a build system that ships with Visual Studio. You are advised to use
 Ninja instead which is significantly faster due to supporting concurrent
@@ -189,6 +206,40 @@ are multi-configuration generators which means you don't set the build type when
 CMake. Instead you set the build type inside Visual Studio. See the "Build Type" section
 for more information.
 
+### General workflow
+
+The general workflow when using CMake is the following
+
+1. Create a new build directory
+2. Configure the project
+3. Generate the build system
+4. Invoke the build system to build the project
+
+To perform steps 2 and 3 you can choose from three different tools
+
+* cmake
+* ccmake
+* cmake-gui
+
+``cmake`` is a command line tool and is what you should use if you are
+writing a script to build Z3. This tool performs steps 1 and 2 in one
+go without user interaction. The ``ccmake`` and ``cmake-gui`` tools are
+more interactive and allow you to change various options. In both these
+tools the basic steps to follow are:
+
+1. Configure.
+2. Change any options you wish. Everytime you change a set of options
+   You should configure again. This may cause new options to appear
+3. Generate.
+
+For information see https://cmake.org/runningcmake/
+
+Note when invoking CMake you give it the path to the source directory.
+This is the top-level directory in the Z3 repository containing a
+``CMakeLists.txt``. That file should contain the line ``project(Z3 C CXX)``.
+If you give it a path deeper into the Z3 repository (e.g. the ``src`` directory)
+the configure step will fail.
+
 ## Build Types
 
 Several build types are supported.
@@ -231,18 +282,56 @@ cmake -DCMAKE_BUILD_TYPE=Release -DENABLE_TRACING=FALSE ../
 
 These notes are help developers and packagers of Z3.
 
+### Boostrapping the CMake build
+
+Z3's CMake system is experimental and not officially supported. Consequently
+Z3's developers have decided that they do not want the CMake files in the
+``src/`` and ``examples/`` folders. Instead the ``contrib/cmake/bootstrap.py``
+script copies or hard links them into the correct locations. For context
+on this decision see https://github.com/Z3Prover/z3/pull/461 .
+
+The ``contrib/cmake/bootstrap.py create`` command just copies over files which makes
+development harder because you have to copy your modifications over to the
+files in ``contrib/cmake`` for your changes to committed to git. If you are on a UNIX like
+platform you can create hard links instead by running
+
+```
+contrib/cmake/boostrap.py create --hard-link
+```
+
+Using hard links means that modifying any of the "copied" files also modifies the
+file under version control. Using hard links also means that the file modification time
+will appear correct (i.e. the hard-linked "copies" have the same file modification time
+as the corresponding file under version control) which means CMake will correctly reconfigure
+when invoked. This is why using symbolic links is not an option because the file modification
+time of a symbolic link is not the same as the file modification of the file being pointed to.
+
+Unfortunately a downside to using hard links (or just plain copies) is that if
+you pull down new code (i.e. ``git pull``) then some of the CMake files under
+version control may change but the corresponding hard-linked "copies" will not.
+
+This mean that (regardless of whether or not you use hard links) every time you
+pull down new code or change branch or do an interactive rebase you must run
+(with or without ``--hard-link``):
+
+```
+contrb/cmake/boostrap.py create
+```
+
+in order to be sure that the copied CMake files are not out of date.
+
 ### Install/Uninstall
 
 Install and uninstall targets are supported. Use ``CMAKE_INSTALL_PREFIX`` to set the install
 prefix.
 
-To install
+To install run
 
 ```
 make install
 ```
 
-To uninstall
+To uninstall run
 
 ```
 make uninstall
diff --git a/contrib/cmake/bootstrap.py b/contrib/cmake/bootstrap.py
new file mode 100755
index 000000000..e9524dad7
--- /dev/null
+++ b/contrib/cmake/bootstrap.py
@@ -0,0 +1,254 @@
+#!/usr/bin/env python
+"""
+This script is used to copy or delete the
+CMake build system files from the contrib/cmake
+folder into the their correct location in the Z3
+repository.
+
+It offers two modes
+
+* create - This will symlink the ``cmake`` directory and copy (or hard link)
+the appropriate files into their correct locations in the repository.
+
+* remove - This will remove the symlinked ``cmake``
+directory and remove the files added by the above
+methods.
+
+This has the advantage
+that editing the hard link edits the underlying file
+(making development easier because copying files is
+not neccessary) and CMake will regenerate correctly
+because the modification time stamps will be correct.
+
+"""
+import argparse
+import logging
+import os
+import pprint
+import shutil
+import sys
+
+def get_full_path_to_script():
+  return os.path.abspath(__file__)
+
+def get_cmake_contrib_dir():
+  return os.path.dirname(get_full_path_to_script())
+
+def get_repo_root_dir():
+  r = os.path.dirname(os.path.dirname(get_cmake_contrib_dir()))
+  assert os.path.isdir(r)
+  return r
+
+# These are paths that should be ignored when checking if a folder
+# in the ``contrib/cmake`` exists in the root of the repository
+verificationExceptions = {
+  os.path.join(get_repo_root_dir(), 'cmake'),
+  os.path.join(get_repo_root_dir(), 'cmake', 'modules')
+}
+
+def contribPathToRepoPath(path):
+  assert path.startswith(get_cmake_contrib_dir())
+  stripped = path[len(get_cmake_contrib_dir()) + 1:] # Plus one is to remove leading slash
+  assert not os.path.isabs(stripped)
+  logging.debug('stripped:{}'.format(stripped))
+  r = os.path.join(get_repo_root_dir(), stripped)
+  assert os.path.isabs(r)
+  logging.debug('Converted contrib path "{}" to repo path "{}"'.format(path, r))
+  return r
+
+def verify_mirrored_directory_struture():
+  """
+  Check that the directories contained in ``contrib/cmake`` exist
+  in the root of the repo.
+  """
+  for (dirpath, _, _) in os.walk(get_cmake_contrib_dir()):
+    expectedDir = contribPathToRepoPath(dirpath)
+    logging.debug('expectedDir:{}'.format(expectedDir))
+    if (not (os.path.exists(expectedDir) and os.path.isdir(expectedDir)) and
+        expectedDir not in verificationExceptions):
+      logging.error(('Expected to find directory "{}" but it does not exist'
+                     ' or is not a directory').format(expectedDir))
+      return 1
+
+  return 0
+
+def mk_sym_link(target, linkName):
+  logging.info('Making symbolic link target="{}", linkName="{}"'.format(target, linkName))
+  if os.path.exists(linkName):
+    logging.info('Removing existing link "{}"'.format(linkName))
+    if not os.path.islink(linkName):
+      logging.warning('"{}" overwriting file that is not a symlink'.format(linkName))
+    delete_path(linkName)
+  if os.name == 'posix':
+    os.symlink(src=target, dst=linkName)
+  else:
+    # TODO: Windows does support symlinks but the implementation to do that
+    # from python is a little complicated so for now lets just copy everyting
+    logging.warning('Creating symbolic links is not supported. Just making a copy instead')
+    if os.path.isdir(target):
+      # Recursively copy directory
+      shutil.copytree(src=target, dst=linkName, symlinks=False, ignore=False)
+    else:
+      # Copy file
+      assert os.path.isfile(target)
+      shutil.copy2(src=target, dst=linkName)
+
+def delete_path(path):
+  logging.info('Removing "{}"'.format(path))
+  if not os.path.exists(path):
+    logging.warning('"{}" does not exist'.format(path))
+    return
+  if os.path.isdir(path) and not os.path.islink(path):
+    # FIXME: If we can get symbolic link support on Windows we
+    # can disallow this completely.
+    assert os.name == 'nt'
+    shutil.rmtree(path)
+  else:
+    os.remove(path)
+
+def shouldSkipFile(path):
+  # Skip this script
+  if path == get_full_path_to_script():
+    return True
+  # Skip the maintainers file
+  if path == os.path.join(get_cmake_contrib_dir(), 'maintainers.txt'):
+    return True
+  # Skip Vim temporary files
+  if os.path.basename(path).startswith('.') and path.endswith('.swp'):
+    return True
+  return False
+
+
+def create(useHardLinks):
+  """
+    Copy or hard link files in the CMake contrib directory
+    into the repository where they are intended to live.
+
+    Note that symbolic links for the CMakeLists.txt files
+    are not appropriate because they won't have the right
+    file modification time when the files they point to
+    are modified. This would prevent CMake from correctly
+    reconfiguring when it detects this is required.
+  """
+
+  # Make the ``cmake`` directory a symbolic link.
+  # We treat this one specially as it is the only directory
+  # that doesn't already exist in the repository root so
+  # we can just use a symlink here
+  linkName = os.path.join(get_repo_root_dir(), 'cmake')
+  target = os.path.join(get_cmake_contrib_dir(), 'cmake')
+  specialDir = target
+  mk_sym_link(target, linkName)
+
+  for (dirPath,_ , fileNames) in os.walk(get_cmake_contrib_dir()):
+    # Skip the special directory and its children
+    if dirPath.startswith(specialDir):
+      logging.info('Skipping directory "{}"'.format(dirPath))
+      continue
+
+    for fileName in fileNames:
+      fileInContrib = os.path.join(dirPath, fileName)
+      # Skip files
+      if shouldSkipFile(fileInContrib):
+        logging.info('Skipping "{}"'.format(fileInContrib))
+        continue
+      fileInRepo = contribPathToRepoPath(fileInContrib)
+      logging.info('"{}" => "{}"'.format(fileInContrib, fileInRepo))
+      if useHardLinks:
+        if not os.name == 'posix':
+          logging.error('Hard links are not supported on your platform')
+          return False
+        if os.path.exists(fileInRepo):
+          delete_path(fileInRepo)
+        os.link(src=fileInContrib, dst=fileInRepo)
+      else:
+        try:
+          shutil.copy2(src=fileInContrib, dst=fileInRepo)
+        except shutil.SameFileError as e:
+          # Can hit this if used created hard links first and then run again without
+          # wanting hard links
+          logging.error('Trying to copy "{}" to "{}" but they are the same file'.format(
+            fileInContrib, fileInRepo))
+          logging.error('You should remove the files using the "remove" mode '
+                        'and try to create again. You probably are mixing the '
+                        'hard-link and non-hard-link create modes')
+          return False
+  return True
+
+def remove():
+  """
+    Remove the CMake files from their intended location in
+    the repository. This is used to remove
+    the files created by the ``create()`` function.
+  """
+  # This directory is treated specially as it is normally
+  # a symlink.
+  linkName = os.path.join(get_repo_root_dir(), 'cmake')
+  delete_path(linkName)
+  specialDir = os.path.join(get_cmake_contrib_dir(), 'cmake')
+
+  for (dirPath,_ , fileNames) in os.walk(get_cmake_contrib_dir()):
+    # Skip the special directory and its children
+    if dirPath.startswith(specialDir):
+      logging.info('Skipping directory "{}"'.format(dirPath))
+      continue
+    for fileName in fileNames:
+      fileInContrib = os.path.join(dirPath, fileName)
+      # Skip files
+      if shouldSkipFile(fileInContrib):
+        logging.info('Skipping "{}"'.format(fileInContrib))
+        continue
+      fileInRepo = contribPathToRepoPath(fileInContrib)
+      if os.path.exists(fileInRepo):
+        logging.info('Removing "{}"'.format(fileInRepo))
+        delete_path(fileInRepo)
+  return True
+
+def main(args):
+  logging.basicConfig(level=logging.INFO)
+  parser = argparse.ArgumentParser(description=__doc__)
+  parser.add_argument('mode',
+    choices=['create', 'remove'],
+    help='The mode to use')
+  parser.add_argument("-l","--log-level",
+    type=str,
+    default="info",
+    dest="log_level",
+    choices=['debug','info','warning','error']
+  )
+  parser.add_argument("-H", "--hard-link",
+    action='store_true',
+    default=False,
+    dest='hard_link',
+    help='When using the create mode create hard links instead of copies'
+  )
+  pargs = parser.parse_args(args)
+
+  logLevel = getattr(logging, pargs.log_level.upper(),None)
+  logging.basicConfig(level=logLevel)
+
+  # Before we start make sure we can transplant the CMake files on to
+  # repository
+  if verify_mirrored_directory_struture() != 0:
+    logging.error('"{}" does not mirror "{}"'.format(get_cmake_contrib_dir(), get_repo_root_dir()))
+    return 1
+
+  if pargs.mode == "create":
+    if not create(useHardLinks=pargs.hard_link):
+      logging.error("Failed to create")
+      return 1
+  elif pargs.mode == "create_hard_link":
+    if not create(useHardLinks=True):
+      logging.error("Failed to create_hard_link")
+      return 1
+  elif pargs.mode == "remove":
+    if not remove():
+      logging.error("Failed to remove")
+      return 1
+  else:
+    logging.error('Unknown mode "{}"'.format(pargs.mode))
+
+  return 0
+
+if __name__ == '__main__':
+  sys.exit(main(sys.argv[1:]))
diff --git a/contrib/cmake/maintainers.txt b/contrib/cmake/maintainers.txt
new file mode 100644
index 000000000..caa6798c6
--- /dev/null
+++ b/contrib/cmake/maintainers.txt
@@ -0,0 +1,3 @@
+# Maintainers
+
+- Dan Liew (@delcypher)