diff --git a/.travis.yml b/.travis.yml
index 5aca4c423ab..7f7a5159bd2 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -137,6 +137,34 @@ jobs:
         - EXTRA_CXXFLAGS="-DDEBUG"
       script: echo "Not running any tests for a debug build."
 
+    - stage: Test different OS/CXX/Flags
+      os: linux
+      cache: ccache
+      env:
+        - BUILD_SYSTEM=cmake
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+          packages:
+            - g++-5
+      install:
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=g++-5'
+        - cmake --build build -- -j4
+      script: (cd build; ctest -V -L CORE)
+
+    - stage: Test different OS/CXX/Flags
+      os: osx
+      cache: ccache
+      env:
+        - BUILD_SYSTEM=cmake
+        - CCACHE_CPP2=yes
+      install:
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
+        - cmake --build build -- -j4
+      script: (cd build; ctest -V -L CORE)
+
+
   allow_failures:
     - <<: *linter-stage
 
diff --git a/CMakeLists.txt b/CMakeLists.txt
new file mode 100644
index 00000000000..a5c0ef6893d
--- /dev/null
+++ b/CMakeLists.txt
@@ -0,0 +1,40 @@
+cmake_minimum_required(VERSION 3.2)
+
+find_program(CCACHE_PROGRAM ccache)
+if(CCACHE_PROGRAM)
+    set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE "${CCACHE_PROGRAM}")
+ endif()
+
+set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
+
+include(GNUInstallDirs)
+
+set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
+
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
+   "${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU"
+)
+    #   Ensure NDEBUG is not set for release builds
+    set(CMAKE_CXX_FLAGS_RELEASE "-O2")
+    #   Enable lots of warnings
+    set(CMAKE_CXX_FLAGS "-Wall -Wpedantic -Werror")
+elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+    #   This would be the place to enable warnings for Windows builds, although
+    #   config.inc doesn't seem to do that currently
+endif()
+
+set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
+
+set(sat_impl "minisat2" CACHE STRING
+    "This setting controls the SAT library which is used. Valid values are 'minisat2' and 'glucose'"
+)
+
+add_subdirectory(src)
+
+if(${enable_cbmc_tests})
+    enable_testing()
+endif()
+add_subdirectory(unit)
+add_subdirectory(regression)
diff --git a/COMPILING b/COMPILING
index 3df46849022..2ec4c482bba 100644
--- a/COMPILING
+++ b/COMPILING
@@ -171,7 +171,7 @@ Follow these instructions:
    BUILD_ENV = MSVC
 
    Open the Visual Studio Command prompt, and then bash.exe -login from
-   Cygwin from in there. 
+   Cygwin from in there.
 
 3) Type cd src; make - that should do it.
 
@@ -183,6 +183,53 @@ can be used for building with MSBuild.  Note that you still need to run
 flex/bison using "make generated_files" before opening the project.
 
 
+WORKING WITH CMAKE (EXPERIMENTAL)
+---------------------------------
+
+There is an experimental build based on CMake instead of hand-written
+makefiles. It should work on a wider variety of systems than the standard
+makefile build, and can integrate better with IDEs and static-analysis tools.
+
+0) Run `cmake --version`. If you get a command-not-found error, or the installed
+   version is lower than 3.2, go and install a new version. Most Linux
+   distributions have a package for CMake, and Mac users can get it through
+   Homebrew.  Windows users should download it manually from cmake.org.
+
+1) Create a directory to store your build:
+   `mkdir build`
+   Run this from the *top level* folder of the project. This is different from
+   the other builds, which require you to `cd src` first.
+
+2) Generate build files with CMake:
+   `cmake -H. -Bbuild`
+   This command tells CMake to use the configuration in the current directory,
+   and to generate build files into the `build` directory.
+   This is the point to specify custom build settings, such as compilers and
+   build back-ends. You can use clang (for example) by adding the argument
+   `-DCMAKE_CXX_COMPILER=clang++` to the command line. You can also tell
+   CMake to generate IDE projects by supplying the `-G` flag.
+   Run `cmake -G` for a comprehensive list of supported back-ends.
+
+   Generally it is not necessary to manually specify individual compiler or
+   linker flags, as CMake defines a number of "build modes" including Debug
+   and Release modes. To build in a particular mode, add the flag
+   `-DCMAKE_BUILD_TYPE=Debug` (or `Release`) to the initial invocation.
+
+   If you *do* need to manually add flags, use `-DCMAKE_CXX_FLAGS=...` and
+   `-DCMAKE_EXE_LINKER_FLAGS=...`. This is useful for enabling clang's
+   sanitizers.
+
+   Finally, to enable building universal binaries on macOS, you can pass the
+   flag `-DCMAKE_OSX_ARCHITECTURES=i386;x86_64`. If you don't supply this flag,
+   the build will just be for the architecture of your machine.
+
+3) Run the build:
+   `cmake --build build`
+   This command tells CMake to invoke the correct tool to run the build in the
+   `build` directory. You can also use the build back-end directly by invoking
+   `make`, `ninja`, or opening the generated IDE project as appropriate.
+
+
 WORKING WITH ECLIPSE
 --------------------
 
diff --git a/appveyor.yml b/appveyor.yml
index 4f28cf54254..f3b42b436d1 100644
--- a/appveyor.yml
+++ b/appveyor.yml
@@ -60,19 +60,6 @@ build_script:
 test_script:
 - cmd: |
     cd regression
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" ansi-c/Makefile
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" cpp/Makefile
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-instrument/chain.sh
-    sed -i "15s/.*/$goto_cc $name.c/" goto-instrument/chain.sh
-    sed -i "16i mv $name.exe $name.gb" goto-instrument/chain.sh
-    sed -i "23s/.*/  $goto_cc ${name}-mod.c/" goto-instrument/chain.sh
-    sed -i "24i   mv ${name}-mod.exe $name-mod.gb" goto-instrument/chain.sh
-    cat goto-instrument/chain.sh
-
-    sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-instrument-typedef/chain.sh || true
-    sed -i "12s/.*/$GC $NAME.c --function fun/" goto-instrument-typedef/chain.sh || true
-    sed -i "13i mv $NAME.exe $NAME.gb" goto-instrument-typedef/chain.sh || true
-    cat goto-instrument-typedef/chain.sh || true
 
     rem HACK disable failing tests
     rmdir /s /q ansi-c\arch_flags_mcpu_bad
diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
new file mode 100644
index 00000000000..245e8611246
--- /dev/null
+++ b/regression/CMakeLists.txt
@@ -0,0 +1,36 @@
+set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD_REQUIRED true)
+
+set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
+
+macro(add_test_pl_profile name cmdline flag profile)
+    add_test(
+        NAME "${name}-${profile}"
+        COMMAND ${test_pl_path} -c ${cmdline} ${flag}
+        WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+    )
+    set_tests_properties("${name}-${profile}" PROPERTIES
+        LABELS "${profile}"
+    )
+endmacro(add_test_pl_profile)
+
+macro(add_test_pl_tests name cmdline)
+    add_test_pl_profile("${name}" "${cmdline}" -C CORE)
+    add_test_pl_profile("${name}" "${cmdline}" -T THOROUGH)
+    add_test_pl_profile("${name}" "${cmdline}" -F FUTURE)
+    add_test_pl_profile("${name}" "${cmdline}" -K KNOWNBUG)
+endmacro(add_test_pl_tests)
+
+add_subdirectory(ansi-c)
+add_subdirectory(cbmc)
+add_subdirectory(cbmc-java)
+add_subdirectory(cbmc-java-inheritance)
+add_subdirectory(cpp)
+add_subdirectory(goto-analyzer)
+add_subdirectory(goto-diff)
+add_subdirectory(goto-instrument)
+add_subdirectory(goto-instrument-typedef)
+add_subdirectory(invariants)
+add_subdirectory(strings)
+add_subdirectory(strings-smoke-tests)
+add_subdirectory(test-script)
diff --git a/regression/ansi-c/CMakeLists.txt b/regression/ansi-c/CMakeLists.txt
new file mode 100644
index 00000000000..027ec188f71
--- /dev/null
+++ b/regression/ansi-c/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "ansi-c"
+    "$<TARGET_FILE:goto-cc>"
+)
diff --git a/regression/ansi-c/Makefile b/regression/ansi-c/Makefile
index 87af55e3306..c770b3b3ed7 100644
--- a/regression/ansi-c/Makefile
+++ b/regression/ansi-c/Makefile
@@ -1,13 +1,22 @@
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+else
+	exe=../../../src/goto-cc/goto-cc
+endif
+
 test:
-	@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
+	@if ! ../test.pl -c $(exe) ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi
 
 tests.log: ../test.pl
-	@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
+	@if ! ../test.pl -c $(exe) ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi
diff --git a/regression/cbmc-java-inheritance/CMakeLists.txt b/regression/cbmc-java-inheritance/CMakeLists.txt
new file mode 100644
index 00000000000..cf949e080b8
--- /dev/null
+++ b/regression/cbmc-java-inheritance/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "cbmc-java-inheritance"
+    "$<TARGET_FILE:cbmc>"
+)
diff --git a/regression/cbmc-java/CMakeLists.txt b/regression/cbmc-java/CMakeLists.txt
new file mode 100644
index 00000000000..37252add85e
--- /dev/null
+++ b/regression/cbmc-java/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "cbmc-java"
+    "$<TARGET_FILE:cbmc>"
+)
diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt
new file mode 100644
index 00000000000..ee9f8f2e90f
--- /dev/null
+++ b/regression/cbmc/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "cbmc"
+    "$<TARGET_FILE:cbmc>"
+)
diff --git a/regression/cpp/CMakeLists.txt b/regression/cpp/CMakeLists.txt
new file mode 100644
index 00000000000..c6eea89555b
--- /dev/null
+++ b/regression/cpp/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "cpp"
+    "$<TARGET_FILE:goto-cc>"
+)
diff --git a/regression/cpp/Makefile b/regression/cpp/Makefile
index 87af55e3306..c770b3b3ed7 100644
--- a/regression/cpp/Makefile
+++ b/regression/cpp/Makefile
@@ -1,13 +1,22 @@
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+else
+	exe=../../../src/goto-cc/goto-cc
+endif
+
 test:
-	@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
+	@if ! ../test.pl -c $(exe) ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi
 
 tests.log: ../test.pl
-	@if ! ../test.pl -c ../../../src/goto-cc/goto-cc ; then \
+	@if ! ../test.pl -c $(exe) ; then \
 		../failed-tests-printer.pl ; \
 		exit 1 ; \
 	fi
diff --git a/regression/goto-analyzer/CMakeLists.txt b/regression/goto-analyzer/CMakeLists.txt
new file mode 100644
index 00000000000..3d5daac5b92
--- /dev/null
+++ b/regression/goto-analyzer/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "goto-analyzer"
+    "$<TARGET_FILE:goto-analyzer>"
+)
diff --git a/regression/goto-diff/CMakeLists.txt b/regression/goto-diff/CMakeLists.txt
new file mode 100644
index 00000000000..9f0957a1386
--- /dev/null
+++ b/regression/goto-diff/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "goto-diff"
+    "$<TARGET_FILE:goto-diff>"
+)
diff --git a/regression/goto-instrument-typedef/CMakeLists.txt b/regression/goto-instrument-typedef/CMakeLists.txt
new file mode 100644
index 00000000000..63a842ccec9
--- /dev/null
+++ b/regression/goto-instrument-typedef/CMakeLists.txt
@@ -0,0 +1,10 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "goto-instrument-typedef"
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> ${is_windows}"
+)
diff --git a/regression/goto-instrument-typedef/Makefile b/regression/goto-instrument-typedef/Makefile
index 08fe97ae88c..56de781ae2c 100644
--- a/regression/goto-instrument-typedef/Makefile
+++ b/regression/goto-instrument-typedef/Makefile
@@ -1,14 +1,24 @@
-
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows="true"
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows="false"
+endif
+
 test:
-	@if ! ../test.pl -c ../chain.sh ; then \
+	@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)' ; then \
 		../failed-tests-printer.pl ; \
 		exit 1; \
 	fi
 
 tests.log:
-	@if ! ../test.pl -c ../chain.sh ; then \
+	@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)' ; then \
 		../failed-tests-printer.pl ; \
 		exit 1; \
 	fi
diff --git a/regression/goto-instrument-typedef/chain.sh b/regression/goto-instrument-typedef/chain.sh
index 9cef4ffdfa4..d53833cccd9 100755
--- a/regression/goto-instrument-typedef/chain.sh
+++ b/regression/goto-instrument-typedef/chain.sh
@@ -1,14 +1,21 @@
 #!/bin/bash
 
-SRC=../../../src
+GC=$1
+GI=$2
+is_windows=$3
 
-GC=$SRC/goto-cc/goto-cc
-GI=$SRC/goto-instrument/goto-instrument
+name=${*:$#}
+name=${name%.c}
 
-OPTS=$1
-NAME=${2%.c}
+args=${*:4:$#-4}
 
-rm $NAME.gb
-$GC $NAME.c --function fun -o $NAME.gb
-echo $GI $OPTS $NAME.gb
-$GI $OPTS $NAME.gb
+rm "${name}.gb"
+if [[ "${is_windows}" == "true" ]]; then
+  "$GC" "${name}.c" --function fun
+  mv "${name}.exe" "${name}.gb"
+else
+  "$GC" "${name}.c" --function fun -o "${name}.gb"
+fi
+
+echo "$GI" ${args} "${name}.gb"
+"$GI" ${args} "${name}.gb"
diff --git a/regression/goto-instrument/CMakeLists.txt b/regression/goto-instrument/CMakeLists.txt
new file mode 100644
index 00000000000..088fcab9651
--- /dev/null
+++ b/regression/goto-instrument/CMakeLists.txt
@@ -0,0 +1,10 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "goto-instrument"
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
+)
diff --git a/regression/goto-instrument/Makefile b/regression/goto-instrument/Makefile
index 94605814b4a..a8d54370285 100644
--- a/regression/goto-instrument/Makefile
+++ b/regression/goto-instrument/Makefile
@@ -1,14 +1,24 @@
-
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows="true"
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows="false"
+endif
+
 test:
-	@if ! ../test.pl -c ../chain.sh ; then \
+	@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' ; then \
 		../failed-tests-printer.pl ; \
 		exit 1; \
 	fi
 
 tests.log:
-	@if ! ../test.pl -c ../chain.sh ; then \
+	@if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' ; then \
 		../failed-tests-printer.pl ; \
 		exit 1; \
 	fi
diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh
index 68f50b095bc..2656ea4488f 100755
--- a/regression/goto-instrument/chain.sh
+++ b/regression/goto-instrument/chain.sh
@@ -2,26 +2,37 @@
 
 set -e
 
-src=../../../src
-goto_cc=$src/goto-cc/goto-cc
-goto_instrument=$src/goto-instrument/goto-instrument
-cbmc=$src/cbmc/cbmc
+goto_cc=$1
+goto_instrument=$2
+cbmc=$3
+is_windows=$4
 
-name=${@:$#}
+name=${*:$#}
 name=${name%.c}
 
-args=${@:1:$#-1}
-
-$goto_cc -o $name.gb $name.c
-# $goto_instrument --show-goto-functions $name.gb
-$goto_instrument $args $name.gb ${name}-mod.gb
-if [ ! -e ${name}-mod.gb ] ; then
-  cp $name.gb ${name}-mod.gb
-elif echo "$args" | grep -q -- "--dump-c" ; then
-  mv ${name}-mod.gb ${name}-mod.c
-  $goto_cc ${name}-mod.c -o ${name}-mod.gb
-  rm ${name}-mod.c
+args=${*:5:$#-5}
+
+if [[ "${is_windows}" == "true" ]]; then
+  $goto_cc "${name}.c"
+  mv "${name}.exe" "${name}.gb"
+else
+  $goto_cc -o "${name}.gb" "${name}.c"
 fi
-$goto_instrument --show-goto-functions ${name}-mod.gb
-$cbmc ${name}-mod.gb
 
+$goto_instrument ${args} "${name}.gb" "${name}-mod.gb"
+if [ ! -e "${name}-mod.gb" ] ; then
+  cp "$name.gb" "${name}-mod.gb"
+elif echo $args | grep -q -- "--dump-c" ; then
+  mv "${name}-mod.gb" "${name}-mod.c"
+
+  if [[ "${is_windows}" == "true" ]]; then
+    $goto_cc "${name}-mod.c"
+    mv "${name}-mod.exe" "${name}-mod.gb"
+  else
+    $goto_cc -o "${name}-mod.gb" "${name}-mod.c"
+  fi
+
+  rm "${name}-mod.c"
+fi
+$goto_instrument --show-goto-functions "${name}-mod.gb"
+$cbmc "${name}-mod.gb"
diff --git a/regression/invariants/CMakeLists.txt b/regression/invariants/CMakeLists.txt
new file mode 100644
index 00000000000..467e2b13950
--- /dev/null
+++ b/regression/invariants/CMakeLists.txt
@@ -0,0 +1,7 @@
+add_executable(driver driver.cpp)
+target_link_libraries(driver big-int util)
+
+add_test_pl_tests(
+    "invariants"
+    "$<TARGET_FILE:driver>"
+)
diff --git a/regression/strings-smoke-tests/CMakeLists.txt b/regression/strings-smoke-tests/CMakeLists.txt
new file mode 100644
index 00000000000..6e8a19a9796
--- /dev/null
+++ b/regression/strings-smoke-tests/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "strings-smoke-test"
+    "$<TARGET_FILE:cbmc>"
+)
diff --git a/regression/strings/CMakeLists.txt b/regression/strings/CMakeLists.txt
new file mode 100644
index 00000000000..846e65ae00d
--- /dev/null
+++ b/regression/strings/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "strings"
+    "$<TARGET_FILE:cbmc>"
+)
diff --git a/regression/test-script/CMakeLists.txt b/regression/test-script/CMakeLists.txt
new file mode 100644
index 00000000000..00ad3a848d6
--- /dev/null
+++ b/regression/test-script/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_test_pl_tests(
+    "test-script"
+    "${CMAKE_CURRENT_SOURCE_DIR}/program_runner.sh" 
+)
diff --git a/scripts/glucose_CMakeLists.txt b/scripts/glucose_CMakeLists.txt
new file mode 100644
index 00000000000..862fc8ba675
--- /dev/null
+++ b/scripts/glucose_CMakeLists.txt
@@ -0,0 +1,30 @@
+cmake_minimum_required(VERSION 3.2)
+
+# CBMC only uses part of glucose.
+# This CMakeLists is designed to build just the parts that are needed.
+
+set(CMAKE_OSX_DEPLOYMENT_TARGET "10.9")
+set(CMAKE_OSX_ARCHITECTURES "i386;x86_64")
+set(CMAKE_BUILD_TYPE RelWithDebInfo)
+
+add_library(glucose-condensed
+    simp/SimpSolver.cc
+    core/Solver.cc
+)
+
+target_include_directories(glucose-condensed
+    PUBLIC
+    $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
+    $<INSTALL_INTERFACE:include>
+)
+
+install(TARGETS glucose-condensed EXPORT glucose-condensed-targets
+    LIBRARY DESTINATION lib
+    ARCHIVE DESTINATION lib
+    RUNTIME DESTINATION bin
+    INCLUDES DESTINATION include
+)
+
+install(DIRECTORY . DESTINATION include FILES_MATCHING PATTERN "*.h")
+
+install(EXPORT glucose-condensed-targets DESTINATION lib/cmake/glucose-condensed)
diff --git a/scripts/minisat2_CMakeLists.txt b/scripts/minisat2_CMakeLists.txt
new file mode 100644
index 00000000000..c749d0e4c8f
--- /dev/null
+++ b/scripts/minisat2_CMakeLists.txt
@@ -0,0 +1,33 @@
+cmake_minimum_required(VERSION 3.2)
+
+# CBMC only uses part of minisat2.
+# This CMakeLists is designed to build just the parts that are needed.
+
+set(CMAKE_OSX_DEPLOYMENT_TARGET "10.9")
+set(CMAKE_OSX_ARCHITECTURES "i386;x86_64")
+set(CMAKE_BUILD_TYPE RelWithDebInfo)
+
+add_library(minisat2-condensed
+    minisat/simp/SimpSolver.cc
+    minisat/core/Solver.cc
+)
+
+set(CBMC_INCLUDE_DIR "" CACHE PATH "The path to CBMC util headers")
+
+target_include_directories(minisat2-condensed
+    PUBLIC
+    $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
+    $<BUILD_INTERFACE:${CBMC_INCLUDE_DIR}>
+    $<INSTALL_INTERFACE:include>
+)
+
+install(TARGETS minisat2-condensed EXPORT minisat-condensed-targets
+    LIBRARY DESTINATION lib
+    ARCHIVE DESTINATION lib
+    RUNTIME DESTINATION bin
+    INCLUDES DESTINATION include
+)
+
+install(DIRECTORY . DESTINATION include FILES_MATCHING PATTERN "*.h")
+
+install(EXPORT minisat-condensed-targets DESTINATION lib/cmake/minisat-condensed)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
new file mode 100644
index 00000000000..a7be2e0fd31
--- /dev/null
+++ b/src/CMakeLists.txt
@@ -0,0 +1,175 @@
+cmake_minimum_required(VERSION 3.2)
+
+#   TODO
+#   -[ ] Install profiles.
+#   -[ ] Specify one of many different solver libraries.
+
+project(CBMC)
+
+set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD_REQUIRED true)
+
+set(CMAKE_EXPORT_COMPILE_COMMANDS true)
+
+find_package(BISON)
+find_package(FLEX)
+
+set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
+
+include(CPack)
+
+find_package(Doxygen)
+if(DOXYGEN_FOUND)
+    add_custom_target(doc
+        "${DOXYGEN_EXECUTABLE}" "${CMAKE_CURRENT_SOURCE_DIR}/doxygen.cfg"
+        WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}"
+    )
+endif(DOXYGEN_FOUND)
+
+#   Add a bison target named 'parser'.
+macro(generic_bison name)
+    bison_target(
+        parser
+        "${CMAKE_CURRENT_SOURCE_DIR}/parser.y"
+        "${CMAKE_CURRENT_BINARY_DIR}/${name}_y.tab.cpp"
+        COMPILE_FLAGS "-pyy${name}"
+    )
+    set(renamed_parser_header "${CMAKE_CURRENT_BINARY_DIR}/${name}_y.tab.h")
+    add_custom_command(OUTPUT "${renamed_parser_header}"
+        COMMAND "${CMAKE_COMMAND}" -E copy "${BISON_parser_OUTPUT_HEADER}" "${renamed_parser_header}"
+        MAIN_DEPENDENCY "${BISON_parser_OUTPUT_HEADER}"
+    )
+    list(REMOVE_ITEM BISON_parser_OUTPUTS "${BISON_parser_OUTPUT_HEADER}")
+    list(APPEND BISON_parser_OUTPUTS "${renamed_parser_header}")
+endmacro(generic_bison)
+
+#   Add a flex target named 'scanner'
+macro(generic_flex name)
+    flex_target(
+        scanner
+        "${CMAKE_CURRENT_SOURCE_DIR}/scanner.l"
+        "${CMAKE_CURRENT_BINARY_DIR}/${name}_lex.yy.cpp"
+        COMPILE_FLAGS "-Pyy${name}"
+    )
+endmacro(generic_flex)
+
+#   Set the public include locations for a target.
+macro(generic_includes name)
+    target_include_directories(${name}
+        PUBLIC
+        ${CBMC_BINARY_DIR}
+        ${CBMC_SOURCE_DIR}
+        ${CMAKE_CURRENT_BINARY_DIR}
+        ${CMAKE_CURRENT_SOURCE_DIR}
+    )
+endmacro(generic_includes)
+
+#   Link optional modules.
+#   Target is the name of the target with optional components.
+#   Name is the name of the optional target.
+#   Also adds a compile flag signalling to the preprocessor that the library is
+#   used.
+macro(add_if_library target name)
+    if(TARGET ${name})
+        target_link_libraries(${target} ${name})
+
+        string(TOUPPER ${name} upper_name)
+        string(REGEX REPLACE "-" "_" define ${upper_name})
+
+        target_compile_definitions(${target} PUBLIC HAVE_${define})
+    endif()
+endmacro(add_if_library)
+
+#   EXTERNAL PROJECTS
+include(ExternalProject)
+set(extern_location ${CMAKE_CURRENT_BINARY_DIR}/extern)
+
+set(extern_include_directory ${extern_location}/include)
+file(MAKE_DIRECTORY ${extern_include_directory})
+
+################################################################################
+
+set(minisat_lib ${extern_location}/lib/${CMAKE_STATIC_LIBRARY_PREFIX}minisat2-condensed${CMAKE_STATIC_LIBRARY_SUFFIX})
+
+#   minisat download: This downloads minisat2, then patches it.  Then, it
+#   injects a minimal CMakeLists.txt so that we can build just the bits we
+#   actually want, without having to update the provided makefile.
+
+ExternalProject_Add(minisat2-extern
+    PREFIX ${extern_location}
+    URL http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
+    PATCH_COMMAND patch -p1 -i ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/minisat-2.2.1-patch
+          COMMAND cmake -E copy ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/minisat2_CMakeLists.txt CMakeLists.txt
+          CMAKE_ARGS -DCMAKE_INSTALL_PREFIX:PATH=<INSTALL_DIR> -DCBMC_INCLUDE_DIR:path=${CMAKE_CURRENT_SOURCE_DIR}
+    BUILD_BYPRODUCTS ${minisat_lib}
+)
+
+add_library(minisat2-condensed STATIC IMPORTED)
+set_target_properties(minisat2-condensed PROPERTIES
+    IMPORTED_LOCATION ${minisat_lib}
+    INTERFACE_INCLUDE_DIRECTORIES "${extern_include_directory}"
+)
+add_dependencies(minisat2-condensed minisat2-extern)
+
+################################################################################
+
+set(glucose_lib ${extern_location}/lib/${CMAKE_STATIC_LIBRARY_PREFIX}glucose-condensed${CMAKE_STATIC_LIBRARY_SUFFIX})
+
+#   glucose download: This downloads glucose, then patches it.  Then, it
+#   injects a minimal CMakeLists.txt so that we can build just the bits we
+#   actually want, without having to update the provided makefile.
+
+ExternalProject_Add(glucose-extern
+    PREFIX ${extern_location}
+    URL http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz
+    PATCH_COMMAND patch -p1 -i ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/glucose-syrup-patch
+          COMMAND cmake -E copy ${CMAKE_CURRENT_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt
+          CMAKE_ARGS -DCMAKE_INSTALL_PREFIX:PATH=<INSTALL_DIR>
+    BUILD_BYPRODUCTS ${glucose_lib}
+)
+
+add_library(glucose-condensed STATIC IMPORTED)
+set_target_properties(glucose-condensed PROPERTIES
+    IMPORTED_LOCATION ${glucose_lib}
+    INTERFACE_INCLUDE_DIRECTORIES "${extern_include_directory}"
+)
+add_dependencies(glucose-condensed glucose-extern)
+
+################################################################################
+
+#   Override add_executable to automatically sign the target on OSX.
+function(add_executable name)
+    _add_executable(${name} ${ARGN})
+    set_target_properties(${name} PROPERTIES XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY
+        "Developer ID Application: Daniel Kroening")
+endfunction(add_executable)
+
+add_subdirectory(analyses)
+add_subdirectory(ansi-c)
+add_subdirectory(assembler)
+add_subdirectory(big-int)
+add_subdirectory(cpp)
+add_subdirectory(goto-programs)
+add_subdirectory(goto-symex)
+add_subdirectory(jsil)
+add_subdirectory(json)
+add_subdirectory(langapi)
+add_subdirectory(linking)
+add_subdirectory(memory-models)
+add_subdirectory(path-symex)
+add_subdirectory(pointer-analysis)
+add_subdirectory(solvers)
+add_subdirectory(util)
+add_subdirectory(xmllang)
+add_subdirectory(java_bytecode)
+add_subdirectory(miniz)
+add_subdirectory(musketeer)
+add_subdirectory(clobber)
+add_subdirectory(cbmc)
+add_subdirectory(goto-cc)
+add_subdirectory(goto-instrument)
+add_subdirectory(symex)
+add_subdirectory(goto-analyzer)
+add_subdirectory(goto-diff)
diff --git a/src/analyses/CMakeLists.txt b/src/analyses/CMakeLists.txt
new file mode 100644
index 00000000000..70922ac2d71
--- /dev/null
+++ b/src/analyses/CMakeLists.txt
@@ -0,0 +1,7 @@
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(analyses ${sources} ${headers})
+
+generic_includes(analyses)
+
+target_link_libraries(analyses util pointer-analysis)
diff --git a/src/ansi-c/CMakeLists.txt b/src/ansi-c/CMakeLists.txt
new file mode 100644
index 00000000000..1e95d1e1e72
--- /dev/null
+++ b/src/ansi-c/CMakeLists.txt
@@ -0,0 +1,97 @@
+generic_bison(ansi_c)
+generic_flex(ansi_c)
+
+add_executable(converter library/converter.cpp)
+
+add_custom_command(OUTPUT converter_input.txt
+    COMMAND cat ${CMAKE_CURRENT_SOURCE_DIR}/library/*.c > converter_input.txt
+)
+
+add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc
+    COMMAND converter < converter_input.txt > ${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc
+    DEPENDS converter_input.txt
+)
+
+add_executable(file_converter file_converter.cpp)
+
+function(make_inc name)
+    add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${name}.inc
+        COMMAND file_converter < ${CMAKE_CURRENT_SOURCE_DIR}/${name}.h > ${CMAKE_CURRENT_BINARY_DIR}/${name}.inc
+    )
+endfunction(make_inc)
+
+################################################################################
+
+if(MINGW)
+    set(platform_unavail
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/java.io.c
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/err.c
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/threads.c
+    )
+else()
+    set(platform_unavail
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/java.io.c
+        ${CMAKE_CURRENT_SOURCE_DIR}/library/threads.c
+    )
+endif()
+
+file(GLOB library_check_sources "library/*.c")
+list(REMOVE_ITEM library_check_sources ${platform_unavail})
+
+add_custom_target(library_check
+    ${CMAKE_CURRENT_SOURCE_DIR}/library_check.sh ${library_check_sources}
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+)
+
+################################################################################
+
+make_inc(arm_builtin_headers)
+make_inc(clang_builtin_headers)
+make_inc(cw_builtin_headers)
+make_inc(gcc_builtin_headers_alpha)
+make_inc(gcc_builtin_headers_arm)
+make_inc(gcc_builtin_headers_generic)
+make_inc(gcc_builtin_headers_ia32)
+make_inc(gcc_builtin_headers_ia32-2)
+make_inc(gcc_builtin_headers_ia32-3)
+make_inc(gcc_builtin_headers_ia32-4)
+make_inc(gcc_builtin_headers_math)
+make_inc(gcc_builtin_headers_mem_string)
+make_inc(gcc_builtin_headers_mips)
+make_inc(gcc_builtin_headers_omp)
+make_inc(gcc_builtin_headers_power)
+make_inc(gcc_builtin_headers_tm)
+make_inc(gcc_builtin_headers_ubsan)
+
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(ansi-c
+    ${sources}
+    ${headers}
+    ${BISON_parser_OUTPUTS}
+    ${FLEX_scanner_OUTPUTS}
+    ${CMAKE_CURRENT_BINARY_DIR}/arm_builtin_headers.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/clang_builtin_headers.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/cw_builtin_headers.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_alpha.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_arm.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_generic.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-2.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-3.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-4.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_math.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_mem_string.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_mips.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_omp.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_power.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_tm.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ubsan.inc
+)
+
+generic_includes(ansi-c)
+
+target_link_libraries(ansi-c util linking goto-programs assembler)
+
+add_dependencies(ansi-c library_check)
diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile
index 58dd5b46025..1cfc9b01385 100644
--- a/src/ansi-c/Makefile
+++ b/src/ansi-c/Makefile
@@ -92,20 +92,7 @@ else
   platform_unavail = library/java.io.c library/threads.c
 endif
 library_check: library/*.c
-	for f in $(filter-out $(platform_unavail), $^) ; do \
-		echo "Checking $$f" ; \
-		cp $$f __libcheck.c ; \
-		perl -p -i -e 's/(__builtin_[^v])/s$$1/' __libcheck.c ; \
-		perl -p -i -e 's/(__sync_)/s$$1/' __libcheck.c ; \
-		perl -p -i -e 's/(__noop)/s$$1/' __libcheck.c ; \
-		$(CC) -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool \
-			-D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c ; \
-		$(CC) -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s \
-			-Wno-unused-label ; \
-		ec=$$? ; \
-		$(RM) __libcheck.s __libcheck.i __libcheck.c ; \
-		[ $$ec -eq 0 ] || exit $$ec ; \
-	done
+	./library_check.sh $(filter-out $(platform_unavail), $^)
 	touch $@
 
 cprover_library.inc: library/converter$(EXEEXT) library/*.c
diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh
new file mode 100755
index 00000000000..c65dcd8919e
--- /dev/null
+++ b/src/ansi-c/library_check.sh
@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+for f in "$@"; do
+    echo "Checking ${f}"
+    cp "${f}" __libcheck.c
+    perl -p -i -e 's/(__builtin_[^v])/s$1/' __libcheck.c
+    perl -p -i -e 's/(__sync_)/s$1/' __libcheck.c
+    perl -p -i -e 's/(__noop)/s$1/' __libcheck.c
+    cc -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
+    cc -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s -Wno-unused-label
+    ec="${?}"
+    rm __libcheck.s __libcheck.i __libcheck.c
+    [ "${ec}" -eq 0 ] || exit "${ec}"
+done
diff --git a/src/assembler/CMakeLists.txt b/src/assembler/CMakeLists.txt
new file mode 100644
index 00000000000..991bcb8fbf6
--- /dev/null
+++ b/src/assembler/CMakeLists.txt
@@ -0,0 +1,13 @@
+generic_flex(assembler)
+
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(assembler
+    ${sources}
+    ${headers}
+    ${FLEX_scanner_OUTPUTS}
+)
+
+generic_includes(assembler)
+
+target_link_libraries(assembler util)
diff --git a/src/big-int/CMakeLists.txt b/src/big-int/CMakeLists.txt
new file mode 100644
index 00000000000..865a8d5edb4
--- /dev/null
+++ b/src/big-int/CMakeLists.txt
@@ -0,0 +1,6 @@
+set(SRC bigint-func.cc bigint.cc)
+
+add_executable(test-bigint ${SRC} bigint-test.cc)
+add_library(big-int ${SRC})
+
+generic_includes(big-int)
diff --git a/src/cbmc/CMakeLists.txt b/src/cbmc/CMakeLists.txt
new file mode 100644
index 00000000000..6777249c8d9
--- /dev/null
+++ b/src/cbmc/CMakeLists.txt
@@ -0,0 +1,39 @@
+# Library
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+list(REMOVE_ITEM sources
+    ${CMAKE_CURRENT_SOURCE_DIR}/cbmc_main.cpp
+)
+add_library(cbmc-lib ${sources} ${headers})
+
+generic_includes(cbmc-lib)
+
+target_link_libraries(cbmc-lib
+    ansi-c
+    cpp
+    linking
+    big-int
+    goto-programs
+    goto-symex
+    pointer-analysis
+    goto-instrument-lib
+    analyses
+    langapi
+    xml
+    assembler
+    solvers
+    util
+    json
+)
+
+add_if_library(cbmc-lib bv_refinement)
+add_if_library(cbmc-lib java_bytecode)
+add_if_library(cbmc-lib jsil)
+add_if_library(cbmc-lib specc)
+add_if_library(cbmc-lib php)
+
+# Executable
+add_executable(cbmc cbmc_main.cpp)
+target_link_libraries(cbmc cbmc-lib)
+
+install(TARGETS cbmc DESTINATION bin)
diff --git a/src/clobber/CMakeLists.txt b/src/clobber/CMakeLists.txt
new file mode 100644
index 00000000000..3d7a43ec9ca
--- /dev/null
+++ b/src/clobber/CMakeLists.txt
@@ -0,0 +1,36 @@
+# Library
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+list(REMOVE_ITEM sources
+    ${CMAKE_CURRENT_SOURCE_DIR}/clobber_main.cpp
+)
+add_library(clobber-lib ${sources} ${headers})
+
+generic_includes(clobber-lib)
+
+target_link_libraries(clobber-lib
+    ansi-c
+    cpp
+    linking
+    big-int
+    goto-programs
+    analyses
+    langapi
+    xml
+    assembler
+    solvers
+    util
+    goto-symex
+    pointer-analysis
+    goto-instrument-lib
+)
+
+add_if_library(clobber-lib bv_refinement)
+add_if_library(clobber-lib java_bytecode)
+add_if_library(clobber-lib specc)
+add_if_library(clobber-lib php)
+
+# Executable
+add_executable(clobber clobber_main.cpp)
+target_link_libraries(clobber clobber-lib)
+
diff --git a/src/common b/src/common
index 2cab9f49cbb..323bdbf4367 100644
--- a/src/common
+++ b/src/common
@@ -33,11 +33,11 @@ endif
   CP_CFLAGS = -MMD -MP
   CXXFLAGS ?= -Wall -O2
 ifeq ($(filter-out OSX OSX_Universal,$(BUILD_ENV_)),)
-  CP_CXXFLAGS = -MMD -MP -mmacosx-version-min=10.9 -std=c++11 -stdlib=libc++
+  CP_CXXFLAGS += -MMD -MP -mmacosx-version-min=10.9 -std=c++11 -stdlib=libc++
   LINKFLAGS += -mmacosx-version-min=10.9 -stdlib=libc++
   LINKNATIVE += -mmacosx-version-min=10.9 -stdlib=libc++
 else
-  CP_CXXFLAGS = -MMD -MP -std=c++11
+  CP_CXXFLAGS += -MMD -MP -std=c++11
 endif
 ifeq ($(filter -O%,$(CXXFLAGS)),)
   CP_CXXFLAGS += -O2
@@ -100,7 +100,7 @@ else ifeq ($(BUILD_ENV_),Cygwin)
   CFLAGS ?= -Wall -O2
   CXXFLAGS ?= -Wall -O2
   CP_CFLAGS = -MMD -MP
-  CP_CXXFLAGS = -MMD -MP -std=c++11 -U__STRICT_ANSI__
+  CP_CXXFLAGS += -MMD -MP -std=c++11 -U__STRICT_ANSI__
   LINKFLAGS = -static -std=c++11
   LINKLIB = ar rcT $@ $^
   LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS) -static
@@ -130,7 +130,7 @@ else ifeq ($(BUILD_ENV_),MSVC)
   CFLAGS ?= /W3 /O2 /GF
   CXXFLAGS ?= /W3 /D_CRT_SECURE_NO_WARNINGS /O2 /GF
   CP_CFLAGS =
-  CP_CXXFLAGS =
+  CP_CXXFLAGS +=
   LINKLIB = lib /NOLOGO /OUT:$@ $^
   LINKBIN = $(CXX) $(LINKFLAGS) /Fe$@ $^ $(LIBS)
   LINKNATIVE = $(HOSTCXX) /Fe$@ $^
diff --git a/src/config.inc b/src/config.inc
index dc2c8f6a47c..5c276dc19c6 100644
--- a/src/config.inc
+++ b/src/config.inc
@@ -26,6 +26,42 @@ MINISAT2 = ../../minisat-2.2.1
 #GLUCOSE = ../../glucose-syrup
 #SMVSAT =
 
+ifneq ($(PRECOSAT),)
+  CP_CXXFLAGS += -DSATCHECK_PRECOSAT
+endif
+
+ifneq ($(PICOSAT),)
+  CP_CXXFLAGS += -DSATCHECK_PICOSAT
+endif
+
+ifneq ($(LINGELING),)
+  CP_CXXFLAGS += -DSATCHECK_LINGELING
+endif
+
+ifneq ($(CHAFF),)
+  CP_CXXFLAGS += -DSATCHECK_CHAFF
+endif
+
+ifneq ($(BOOLEFORCE),)
+  CP_CXXFLAGS += -DSATCHECK_BOOLEFORCE
+endif
+
+ifneq ($(MINISAT),)
+  CP_CXXFLAGS += -DSATCHECK_MINISAT
+endif
+
+ifneq ($(MINISAT2),)
+  CP_CXXFLAGS += -DSATCHECK_MINISAT2
+endif
+
+ifneq ($(GLUCOSE),)
+  CP_CXXFLAGS += -DSATCHECK_GLUCOSE
+endif
+
+ifneq ($(SMVSAT),)
+  CP_CXXFLAGS += -DSATCHECK_SMVSAT
+endif
+
 # Signing identity for MacOS Gatekeeper
 
 OSX_IDENTITY="Developer ID Application: Daniel Kroening"
diff --git a/src/cpp/CMakeLists.txt b/src/cpp/CMakeLists.txt
new file mode 100644
index 00000000000..740c600641b
--- /dev/null
+++ b/src/cpp/CMakeLists.txt
@@ -0,0 +1,7 @@
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(cpp ${sources} ${headers}) 
+
+generic_includes(cpp)
+
+target_link_libraries(cpp util ansi-c)
diff --git a/src/goto-analyzer/CMakeLists.txt b/src/goto-analyzer/CMakeLists.txt
new file mode 100644
index 00000000000..1e07f53afbe
--- /dev/null
+++ b/src/goto-analyzer/CMakeLists.txt
@@ -0,0 +1,32 @@
+# Library
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+list(REMOVE_ITEM sources
+    ${CMAKE_CURRENT_SOURCE_DIR}/goto_analyzer_main.cpp
+)
+add_library(goto-analyzer-lib ${sources} ${headers})
+
+generic_includes(goto-analyzer-lib)
+
+target_link_libraries(goto-analyzer-lib
+    ansi-c
+    cpp
+    linking
+    big-int
+    goto-programs
+    analyses
+    pointer-analysis
+    langapi
+    json
+    assembler
+    util
+)
+
+add_if_library(goto-analyzer-lib java_bytecode)
+add_if_library(goto-analyzer-lib jsil)
+add_if_library(goto-analyzer-lib specc)
+add_if_library(goto-analyzer-lib php)
+
+# Executable
+add_executable(goto-analyzer goto_analyzer_main.cpp)
+target_link_libraries(goto-analyzer goto-analyzer-lib)
diff --git a/src/goto-cc/CMakeLists.txt b/src/goto-cc/CMakeLists.txt
new file mode 100644
index 00000000000..7d7a2d579da
--- /dev/null
+++ b/src/goto-cc/CMakeLists.txt
@@ -0,0 +1,32 @@
+# Library
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+list(REMOVE_ITEM sources
+    ${CMAKE_CURRENT_SOURCE_DIR}/goto_cc_main.cpp
+)
+add_library(goto-cc-lib ${sources} ${headers})
+
+generic_includes(goto-cc-lib)
+
+target_link_libraries(goto-cc-lib
+    big-int
+    goto-programs
+    util
+    linking
+    ansi-c
+    cpp
+    xml
+    assembler
+    langapi
+)
+
+add_if_library(goto-cc-lib java_bytecode)
+add_if_library(goto-cc-lib jsil)
+
+# Executable
+add_executable(goto-cc goto_cc_main.cpp)
+target_link_libraries(goto-cc goto-cc-lib)
+
+if(WIN32)
+  set_target_properties(goto-cc PROPERTIES OUTPUT_NAME goto-cl)
+endif()
diff --git a/src/goto-diff/CMakeLists.txt b/src/goto-diff/CMakeLists.txt
new file mode 100644
index 00000000000..a590e4d9df2
--- /dev/null
+++ b/src/goto-diff/CMakeLists.txt
@@ -0,0 +1,32 @@
+# Library
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+list(REMOVE_ITEM sources
+    ${CMAKE_CURRENT_SOURCE_DIR}/goto_diff_main.cpp
+)
+add_library(goto-diff-lib ${sources} ${headers})
+
+generic_includes(goto-diff-lib)
+
+target_link_libraries(goto-diff-lib
+    ansi-c
+    cpp
+    linking
+    big-int
+    pointer-analysis
+    goto-programs
+    assembler
+    analyses
+    langapi
+    xml
+    util
+    solvers
+)
+
+add_if_library(goto-diff-lib java_bytecode)
+add_if_library(goto-diff-lib jsil)
+add_if_library(goto-diff-lib php)
+
+# Executable
+add_executable(goto-diff goto_diff_main.cpp)
+target_link_libraries(goto-diff goto-diff-lib)
diff --git a/src/goto-instrument/CMakeLists.txt b/src/goto-instrument/CMakeLists.txt
new file mode 100644
index 00000000000..233a3bbec41
--- /dev/null
+++ b/src/goto-instrument/CMakeLists.txt
@@ -0,0 +1,36 @@
+# Library
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+list(REMOVE_ITEM sources
+    ${CMAKE_CURRENT_SOURCE_DIR}/goto_instrument_main.cpp
+
+    # This doesn't build
+    ${CMAKE_CURRENT_SOURCE_DIR}/accelerate/linearize.cpp
+)
+add_library(goto-instrument-lib ${sources} ${headers})
+
+generic_includes(goto-instrument-lib)
+
+target_link_libraries(goto-instrument-lib
+    ansi-c
+    cpp
+    linking
+    big-int
+    goto-programs
+    goto-symex
+    assembler
+    pointer-analysis
+    analyses
+    langapi
+    xml
+    util
+    json
+    solvers
+)
+
+add_if_library(goto-instrument-lib java_bytecode)
+add_if_library(goto-instrument-lib glpk)
+
+# Executable
+add_executable(goto-instrument goto_instrument_main.cpp)
+target_link_libraries(goto-instrument goto-instrument-lib)
diff --git a/src/goto-programs/CMakeLists.txt b/src/goto-programs/CMakeLists.txt
new file mode 100644
index 00000000000..84a06943b98
--- /dev/null
+++ b/src/goto-programs/CMakeLists.txt
@@ -0,0 +1,7 @@
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(goto-programs ${sources} ${headers})
+
+generic_includes(goto-programs)
+
+target_link_libraries(goto-programs util assembler langapi analyses ansi-c)
diff --git a/src/goto-symex/CMakeLists.txt b/src/goto-symex/CMakeLists.txt
new file mode 100644
index 00000000000..cc51bb603d9
--- /dev/null
+++ b/src/goto-symex/CMakeLists.txt
@@ -0,0 +1,7 @@
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(goto-symex ${sources} ${headers})
+
+generic_includes(goto-symex)
+
+target_link_libraries(goto-symex util)
diff --git a/src/java_bytecode/CMakeLists.txt b/src/java_bytecode/CMakeLists.txt
new file mode 100644
index 00000000000..282519dbf1c
--- /dev/null
+++ b/src/java_bytecode/CMakeLists.txt
@@ -0,0 +1,7 @@
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(java_bytecode ${sources} ${headers})
+
+generic_includes(java_bytecode)
+
+target_link_libraries(java_bytecode util goto-programs miniz json)
diff --git a/src/jsil/CMakeLists.txt b/src/jsil/CMakeLists.txt
new file mode 100644
index 00000000000..b3a34114639
--- /dev/null
+++ b/src/jsil/CMakeLists.txt
@@ -0,0 +1,15 @@
+generic_bison(jsil)
+generic_flex(jsil)
+
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(jsil
+    ${sources}
+    ${headers}
+    ${BISON_parser_OUTPUTS}
+    ${FLEX_scanner_OUTPUTS}
+)
+
+generic_includes(jsil)
+
+target_link_libraries(jsil util)
diff --git a/src/json/CMakeLists.txt b/src/json/CMakeLists.txt
new file mode 100644
index 00000000000..944085707a0
--- /dev/null
+++ b/src/json/CMakeLists.txt
@@ -0,0 +1,15 @@
+generic_bison(json)
+generic_flex(json)
+
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(json 
+    ${sources}
+    ${headers}
+    ${BISON_parser_OUTPUTS}
+    ${FLEX_scanner_OUTPUTS}
+)
+
+generic_includes(json)
+
+target_link_libraries(json util)
diff --git a/src/langapi/CMakeLists.txt b/src/langapi/CMakeLists.txt
new file mode 100644
index 00000000000..aa71bc63612
--- /dev/null
+++ b/src/langapi/CMakeLists.txt
@@ -0,0 +1,7 @@
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(langapi ${sources} ${headers})
+
+generic_includes(langapi)
+
+target_link_libraries(langapi util)
diff --git a/src/linking/CMakeLists.txt b/src/linking/CMakeLists.txt
new file mode 100644
index 00000000000..f96361799db
--- /dev/null
+++ b/src/linking/CMakeLists.txt
@@ -0,0 +1,7 @@
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(linking ${sources} ${headers})
+
+generic_includes(linking)
+
+target_link_libraries(linking util ansi-c)
diff --git a/src/memory-models/CMakeLists.txt b/src/memory-models/CMakeLists.txt
new file mode 100644
index 00000000000..04e51ad62b1
--- /dev/null
+++ b/src/memory-models/CMakeLists.txt
@@ -0,0 +1,15 @@
+generic_bison(mm)
+generic_flex(mm)
+
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(mmcc
+    ${sources}
+    ${headers}
+    ${BISON_parser_OUTPUTS}
+    ${FLEX_scanner_OUTPUTS}
+)
+
+generic_includes(mmcc)
+
+target_link_libraries(mmcc util)
diff --git a/src/miniz/CMakeLists.txt b/src/miniz/CMakeLists.txt
new file mode 100644
index 00000000000..1d7862730e0
--- /dev/null
+++ b/src/miniz/CMakeLists.txt
@@ -0,0 +1,7 @@
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(miniz ${sources} ${headers})
+
+generic_includes(miniz)
+
+target_link_libraries(miniz)
diff --git a/src/musketeer/CMakeLists.txt b/src/musketeer/CMakeLists.txt
new file mode 100644
index 00000000000..6265183ee0b
--- /dev/null
+++ b/src/musketeer/CMakeLists.txt
@@ -0,0 +1,30 @@
+# Library
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+list(REMOVE_ITEM sources
+    ${CMAKE_CURRENT_SOURCE_DIR}/musketeer_main.cpp
+)
+add_library(musketeer-lib ${sources} ${headers})
+
+generic_includes(musketeer-lib)
+
+target_link_libraries(musketeer-lib
+    ansi-c
+    linking
+    big-int
+    goto-programs
+    goto-symex
+    assembler
+    pointer-analysis
+    analyses
+    langapi
+    util
+    solvers
+    goto-instrument-lib
+)
+
+add_if_library(musketeer-lib glpk)
+
+# Executable
+add_executable(musketeer musketeer_main.cpp)
+target_link_libraries(musketeer musketeer-lib)
diff --git a/src/path-symex/CMakeLists.txt b/src/path-symex/CMakeLists.txt
new file mode 100644
index 00000000000..c86e9c27a25
--- /dev/null
+++ b/src/path-symex/CMakeLists.txt
@@ -0,0 +1,7 @@
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(path-symex ${sources} ${headers})
+
+generic_includes(path-symex)
+
+target_link_libraries(path-symex util pointer-analysis)
diff --git a/src/pointer-analysis/CMakeLists.txt b/src/pointer-analysis/CMakeLists.txt
new file mode 100644
index 00000000000..66d9f23893d
--- /dev/null
+++ b/src/pointer-analysis/CMakeLists.txt
@@ -0,0 +1,7 @@
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(pointer-analysis ${sources} ${headers})
+
+generic_includes(pointer-analysis)
+
+target_link_libraries(pointer-analysis util analyses goto-programs)
diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
new file mode 100644
index 00000000000..910b39f7c6e
--- /dev/null
+++ b/src/solvers/CMakeLists.txt
@@ -0,0 +1,84 @@
+#   We may use one of several different solver libraries.
+#   The following files wrap the chosen solver library.
+#   We remove them all from the solver-library sources list, and then add the
+#   ones we actually need back in.
+set(chaff_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_zchaff.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_zcore.cpp
+)
+set(minisat_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_minisat.cpp
+)
+set(minisat2_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_minisat2.cpp
+)
+set(glucose_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_glucose.cpp
+)
+set(smvsat_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_smvsat.cpp
+)
+set(squolem2_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_squolem.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_squolem_core.cpp
+)
+set(cudd_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_bdd_core.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/qbf/qbf_skizzo_core.cpp
+)
+set(precosat_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_precosat.cpp
+)
+set(picosat_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_picosat.cpp
+)
+set(lingeling_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_lingeling.cpp
+)
+set(booleforce_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_booleforce.cpp
+)
+set(minibdd_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/miniBDD/example.cpp
+)
+set(limmat_source
+    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_limmat.cpp
+)
+
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+list(REMOVE_ITEM sources
+    ${chaff_source}
+    ${minisat_source}
+    ${minisat2_source}
+    ${glucose_source}
+    ${smvsat_source}
+    ${squolem2_source}
+    ${cudd_source}
+    ${precosat_source}
+    ${picosat_source}
+    ${lingeling_source}
+    ${booleforce_source}
+    ${minibdd_source}
+    ${limmat_source}
+)
+
+add_library(solvers ${sources} ${headers})
+
+if("${sat_impl}" STREQUAL "minisat2")
+    message(STATUS "Building solvers with minisat2")
+    target_sources(solvers PRIVATE ${minisat2_source})
+    add_dependencies(solvers minisat2-extern)
+    target_compile_definitions(solvers PUBLIC SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS)
+    target_link_libraries(solvers minisat2-condensed)
+elseif("${sat_impl}" STREQUAL "glucose")
+    message(STATUS "Building solvers with glucose")
+    target_sources(solvers PRIVATE ${glucose_source})
+    add_dependencies(solvers glucose-extern)
+    target_compile_definitions(solvers PUBLIC SATCHECK_GLUCOSE HAVE_GLUCOSE __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS)
+    target_link_libraries(solvers glucose-condensed)
+endif()
+
+target_link_libraries(solvers util)
+
+generic_includes(solvers)
diff --git a/src/solvers/sat/satcheck.h b/src/solvers/sat/satcheck.h
index ada65d253e8..4905f3195ee 100644
--- a/src/solvers/sat/satcheck.h
+++ b/src/solvers/sat/satcheck.h
@@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 // #define SATCHECK_ZCHAFF
 // #define SATCHECK_MINISAT1
-#define SATCHECK_MINISAT2
+// #define SATCHECK_MINISAT2
 // #define SATCHECK_GLUCOSE
 // #define SATCHECK_BOOLEFORCE
 // #define SATCHECK_PRECOSAT
diff --git a/src/solvers/sat/satcheck_glucose.cpp b/src/solvers/sat/satcheck_glucose.cpp
index 3d6e2ae3934..fa146d09414 100644
--- a/src/solvers/sat/satcheck_glucose.cpp
+++ b/src/solvers/sat/satcheck_glucose.cpp
@@ -114,7 +114,7 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
 template<typename T>
 propt::resultt satcheck_glucose_baset<T>::prop_solve()
 {
-  assert(status!=ERROR);
+  assert(status!=statust::ERROR);
 
   // We start counting at 1, thus there is one variable fewer.
   {
@@ -153,9 +153,8 @@ propt::resultt satcheck_glucose_baset<T>::prop_solve()
       {
         messaget::status() <<
           "SAT checker: instance is SATISFIABLE" << eom;
-        assert(!solver->model.empty());
-        status=SAT;
-        return P_SATISFIABLE;
+        status=statust::SAT;
+        return resultt::P_SATISFIABLE;
       }
       else
       {
@@ -165,8 +164,8 @@ propt::resultt satcheck_glucose_baset<T>::prop_solve()
     }
   }
 
-  status=UNSAT;
-  return P_UNSATISFIABLE;
+  status=statust::UNSAT;
+  return resultt::P_UNSATISFIABLE;
 }
 
 template<typename T>
diff --git a/src/symex/CMakeLists.txt b/src/symex/CMakeLists.txt
new file mode 100644
index 00000000000..d4450e79a37
--- /dev/null
+++ b/src/symex/CMakeLists.txt
@@ -0,0 +1,35 @@
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+list(REMOVE_ITEM sources
+    ${CMAKE_CURRENT_SOURCE_DIR}/symex_main.cpp
+)
+add_library(symex-lib ${sources} ${headers})
+
+target_link_libraries(symex-lib
+    ansi-c
+    cpp
+    linking
+    big-int
+    goto-programs
+    analyses
+    langapi
+    xml
+    assembler
+    solvers
+    util
+    goto-symex
+    pointer-analysis
+    goto-instrument-lib
+    path-symex
+)
+
+generic_includes(symex-lib)
+
+add_if_library(symex-lib bv_refinement)
+add_if_library(symex-lib java_bytecode)
+add_if_library(symex-lib specc)
+add_if_library(symex-lib php)
+
+add_executable(symex symex_main.cpp)
+
+target_link_libraries(symex symex-lib)
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
new file mode 100644
index 00000000000..b073a8baa0e
--- /dev/null
+++ b/src/util/CMakeLists.txt
@@ -0,0 +1,7 @@
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(util ${sources} ${headers})
+
+generic_includes(util)
+
+target_link_libraries(util big-int)
diff --git a/src/xmllang/CMakeLists.txt b/src/xmllang/CMakeLists.txt
new file mode 100644
index 00000000000..58879cdee74
--- /dev/null
+++ b/src/xmllang/CMakeLists.txt
@@ -0,0 +1,15 @@
+generic_bison(xml)
+generic_flex(xml)
+
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+add_library(xml 
+    ${sources}
+    ${headers}
+    ${BISON_parser_OUTPUTS}
+    ${FLEX_scanner_OUTPUTS}
+)
+
+generic_includes(xml)
+
+target_link_libraries(xml util)
diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt
new file mode 100644
index 00000000000..623e57ecb50
--- /dev/null
+++ b/unit/CMakeLists.txt
@@ -0,0 +1,72 @@
+set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD_REQUIRED true)
+
+file(GLOB_RECURSE sources "*.cpp")
+file(GLOB_RECURSE headers "*.h")
+list(REMOVE_ITEM sources
+    # Used in executables
+    ${CMAKE_CURRENT_SOURCE_DIR}/miniBDD.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/string_utils.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/sharing_node.cpp
+
+    # Don't build
+    ${CMAKE_CURRENT_SOURCE_DIR}/sharing_map.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/elf_reader.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/smt2_parser.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/json.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/cpp_parser.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/osx_fat_reader.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/unicode.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/wp.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/cpp_scanner.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/float_utils.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/ieee_float.cpp
+)
+
+add_executable(unit ${sources} ${headers})
+target_include_directories(unit
+    PUBLIC
+    ${CBMC_BINARY_DIR}
+    ${CBMC_SOURCE_DIR}
+    ${CMAKE_CURRENT_SOURCE_DIR}
+)
+target_link_libraries(unit ansi-c solvers java_bytecode)
+add_test(
+    NAME unit
+    COMMAND $<TARGET_FILE:unit>
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+)
+set_tests_properties(unit PROPERTIES LABELS CORE)
+
+add_executable(miniBDD miniBDD.cpp)
+target_include_directories(miniBDD
+    PUBLIC
+    ${CBMC_BINARY_DIR}
+    ${CBMC_SOURCE_DIR}
+    ${CMAKE_CURRENT_SOURCE_DIR}
+)
+target_link_libraries(miniBDD solvers ansi-c)
+add_test(NAME miniBDD COMMAND $<TARGET_FILE:miniBDD>)
+set_tests_properties(miniBDD PROPERTIES LABELS CORE)
+
+add_executable(string_utils string_utils.cpp)
+target_include_directories(string_utils
+    PUBLIC
+    ${CBMC_BINARY_DIR}
+    ${CBMC_SOURCE_DIR}
+    ${CMAKE_CURRENT_SOURCE_DIR}
+)
+target_link_libraries(string_utils solvers ansi-c)
+add_test(NAME string_utils COMMAND $<TARGET_FILE:string_utils>)
+set_tests_properties(string_utils PROPERTIES LABELS CORE)
+
+add_executable(sharing_node sharing_node.cpp)
+target_include_directories(sharing_node
+    PUBLIC
+    ${CBMC_BINARY_DIR}
+    ${CBMC_SOURCE_DIR}
+    ${CMAKE_CURRENT_SOURCE_DIR}
+)
+target_link_libraries(sharing_node util)
+add_test(NAME sharing_node COMMAND $<TARGET_FILE:sharing_node>)
+set_tests_properties(sharing_node PROPERTIES LABELS CORE)