cmake: Added initial build infrastructure.

121 files changed, 142 insertions, 0 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
new file mode 100644
index 000000000..9e3580fbb
--- /dev/null
+++ b/CMakeLists.txt
@@ -0,0 +1,23 @@
+cmake_minimum_required (VERSION 2.8.9)
+
+macro(add_cxx_flag flag)
+  message(STATUS "Configure with flag '${flag}'")
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}")
+endmacro()
+
+project (cvc4)
+
+set (CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
+
+# TODO: cln
+find_package(GMP REQUIRED)
+set(LIBRARIES ${LIBRARIES} ${GMP_LIBRARIES})
+include_directories(${GMP_INCLUDE_DIR})
+
+add_subdirectory(src)
+add_subdirectory(test)
+#TODO only if with-lfsc
+#add_subdirectory(proofs/signatures)
+
+#TODO make dist (subdir: examples)
+
diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake
new file mode 100644
index 000000000..4325f666e
--- /dev/null
+++ b/cmake/FindGMP.cmake
@@ -0,0 +1,12 @@
+# Try to find the GMP librairies
+# GMP_FOUND - system has GMP lib
+# GMP_INCLUDE_DIR - the GMP include directory
+# GMP_LIBRARIES - Libraries needed to use GMP
+
+find_path(GMP_INCLUDE_DIR NAMES gmp.h)
+find_library(GMP_LIBRARIES NAMES gmp libgmp)
+
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES)
+
+mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARIES)
diff --git a/contrib/CMakeLists.txt b/contrib/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/contrib/CMakeLists.txt
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/examples/CMakeLists.txt
diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/examples/api/CMakeLists.txt
diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/examples/api/java/CMakeLists.txt
diff --git a/examples/hashsmt/CMakeLists.txt b/examples/hashsmt/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/examples/hashsmt/CMakeLists.txt
diff --git a/examples/nra-translate/CMakeLists.txt b/examples/nra-translate/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/examples/nra-translate/CMakeLists.txt
diff --git a/examples/sets-translate/CMakeLists.txt b/examples/sets-translate/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/examples/sets-translate/CMakeLists.txt
diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/proofs/signatures/CMakeLists.txt
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
new file mode 100644
index 000000000..26e93f8b5
--- /dev/null
+++ b/src/CMakeLists.txt
@@ -0,0 +1,17 @@
+add_subdirectory(base)
+add_subdirectory(bindings)
+add_subdirectory(compat)
+add_subdirectory(context)
+add_subdirectory(decision)
+add_subdirectory(expr)
+add_subdirectory(lib)
+add_subdirectory(main)
+add_subdirectory(options)
+add_subdirectory(parser)
+add_subdirectory(printer)
+add_subdirectory(proof)
+add_subdirectory(prop)
+add_subdirectory(smt)
+add_subdirectory(smt_util)
+add_subdirectory(theory)
+add_subdirectory(util)
diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/base/CMakeLists.txt
diff --git a/src/bindings/CMakeLists.txt b/src/bindings/CMakeLists.txt
new file mode 100644
index 000000000..910b62766
--- /dev/null
+++ b/src/bindings/CMakeLists.txt
@@ -0,0 +1 @@
+add_subdirectory(compat)
diff --git a/src/bindings/compat/CMakeLists.txt b/src/bindings/compat/CMakeLists.txt
new file mode 100644
index 000000000..92c37023a
--- /dev/null
+++ b/src/bindings/compat/CMakeLists.txt
@@ -0,0 +1,2 @@
+add_subdirectory(c)
+add_subdirectory(java)
diff --git a/src/bindings/compat/c/CMakeLists.txt b/src/bindings/compat/c/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/bindings/compat/c/CMakeLists.txt
diff --git a/src/bindings/compat/java/CMakeLists.txt b/src/bindings/compat/java/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/bindings/compat/java/CMakeLists.txt
diff --git a/src/compat/CMakeLists.txt b/src/compat/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/compat/CMakeLists.txt
diff --git a/src/context/CMakeLists.txt b/src/context/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/context/CMakeLists.txt
diff --git a/src/decision/CMakeLists.txt b/src/decision/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/decision/CMakeLists.txt
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/expr/CMakeLists.txt
diff --git a/src/lib/CMakeLists.txt b/src/lib/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/lib/CMakeLists.txt
diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/main/CMakeLists.txt
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/options/CMakeLists.txt
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
new file mode 100644
index 000000000..dcb580d8f
--- /dev/null
+++ b/src/parser/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_subdirectory(cvc)
+add_subdirectory(smt1)
+add_subdirectory(smt2)
+add_subdirectory(tptp)
diff --git a/src/parser/cvc/CMakeLists.txt b/src/parser/cvc/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/parser/cvc/CMakeLists.txt
diff --git a/src/parser/smt1/CMakeLists.txt b/src/parser/smt1/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/parser/smt1/CMakeLists.txt
diff --git a/src/parser/smt2/CMakeLists.txt b/src/parser/smt2/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/parser/smt2/CMakeLists.txt
diff --git a/src/parser/tptp/CMakeLists.txt b/src/parser/tptp/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/parser/tptp/CMakeLists.txt
diff --git a/src/printer/CMakeLists.txt b/src/printer/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/printer/CMakeLists.txt
diff --git a/src/proof/CMakeLists.txt b/src/proof/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/proof/CMakeLists.txt
diff --git a/src/prop/CMakeLists.txt b/src/prop/CMakeLists.txt
new file mode 100644
index 000000000..c7868e0f0
--- /dev/null
+++ b/src/prop/CMakeLists.txt
@@ -0,0 +1,2 @@
+add_subdirectory(bvminisat)
+add_subdirectory(minisat)
diff --git a/src/prop/bvminisat/CMakeLists.txt b/src/prop/bvminisat/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/prop/bvminisat/CMakeLists.txt
diff --git a/src/prop/minisat/CMakeLists.txt b/src/prop/minisat/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/prop/minisat/CMakeLists.txt
diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/smt/CMakeLists.txt
diff --git a/src/smt_util/CMakeLists.txt b/src/smt_util/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/smt_util/CMakeLists.txt
diff --git a/src/theory/CMakeLists.txt b/src/theory/CMakeLists.txt
new file mode 100644
index 000000000..01a98aff8
--- /dev/null
+++ b/src/theory/CMakeLists.txt
@@ -0,0 +1,14 @@
+add_subdirectory(arith)
+add_subdirectory(arrays)
+add_subdirectory(booleans)
+add_subdirectory(builtin)
+add_subdirectory(bv)
+add_subdirectory(datatypes)
+add_subdirectory(example)
+add_subdirectory(fp)
+add_subdirectory(idl)
+add_subdirectory(quantifiers)
+add_subdirectory(sep)
+add_subdirectory(sets)
+add_subdirectory(strings)
+add_subdirectory(uf)
diff --git a/src/theory/arith/CMakeLists.txt b/src/theory/arith/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/theory/arith/CMakeLists.txt
diff --git a/src/theory/arrays/CMakeLists.txt b/src/theory/arrays/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/theory/arrays/CMakeLists.txt
diff --git a/src/theory/booleans/CMakeLists.txt b/src/theory/booleans/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/theory/booleans/CMakeLists.txt
diff --git a/src/theory/builtin/CMakeLists.txt b/src/theory/builtin/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/theory/builtin/CMakeLists.txt
diff --git a/src/theory/bv/CMakeLists.txt b/src/theory/bv/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/theory/bv/CMakeLists.txt
diff --git a/src/theory/datatypes/CMakeLists.txt b/src/theory/datatypes/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/theory/datatypes/CMakeLists.txt
diff --git a/src/theory/example/CMakeLists.txt b/src/theory/example/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/theory/example/CMakeLists.txt
diff --git a/src/theory/fp/CMakeLists.txt b/src/theory/fp/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/theory/fp/CMakeLists.txt
diff --git a/src/theory/idl/CMakeLists.txt b/src/theory/idl/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/theory/idl/CMakeLists.txt
diff --git a/src/theory/quantifiers/CMakeLists.txt b/src/theory/quantifiers/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/theory/quantifiers/CMakeLists.txt
diff --git a/src/theory/sep/CMakeLists.txt b/src/theory/sep/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/theory/sep/CMakeLists.txt
diff --git a/src/theory/sets/CMakeLists.txt b/src/theory/sets/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/theory/sets/CMakeLists.txt
diff --git a/src/theory/strings/CMakeLists.txt b/src/theory/strings/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/theory/strings/CMakeLists.txt
diff --git a/src/theory/uf/CMakeLists.txt b/src/theory/uf/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/theory/uf/CMakeLists.txt
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/src/util/CMakeLists.txt
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
new file mode 100644
index 000000000..07c36b305
--- /dev/null
+++ b/test/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_subdirectory(java)
+add_subdirectory(regress)
+add_subdirectory(system)
+add_subdirectory(unit)
diff --git a/test/java/CMakeLists.txt b/test/java/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/java/CMakeLists.txt
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
new file mode 100644
index 000000000..d69d74cf8
--- /dev/null
+++ b/test/regress/CMakeLists.txt
@@ -0,0 +1,5 @@
+add_subdirectory(regress0)
+add_subdirectory(regress1)
+add_subdirectory(regress2)
+add_subdirectory(regress3)
+add_subdirectory(regress4)
diff --git a/test/regress/regress0/CMakeLists.txt b/test/regress/regress0/CMakeLists.txt
new file mode 100644
index 000000000..5b0bc398d
--- /dev/null
+++ b/test/regress/regress0/CMakeLists.txt
@@ -0,0 +1,27 @@
+add_subdirectory(arith)
+add_subdirectory(arrays)
+add_subdirectory(aufbv)
+add_subdirectory(auflia)
+add_subdirectory(bv)
+add_subdirectory(datatypes)
+add_subdirectory(decision)
+add_subdirectory(expect)
+add_subdirectory(fmf)
+add_subdirectory(lemmas)
+add_subdirectory(nl)
+add_subdirectory(parser)
+add_subdirectory(precedence)
+add_subdirectory(preprocess)
+add_subdirectory(push-pop)
+add_subdirectory(quantifiers)
+add_subdirectory(rels)
+add_subdirectory(rewriterules)
+add_subdirectory(sep)
+add_subdirectory(sets)
+add_subdirectory(strings)
+add_subdirectory(sygus)
+add_subdirectory(tptp)
+add_subdirectory(uf)
+add_subdirectory(uflia)
+add_subdirectory(uflra)
+add_subdirectory(unconstrained)
diff --git a/test/regress/regress0/arith/CMakeLists.txt b/test/regress/regress0/arith/CMakeLists.txt
new file mode 100644
index 000000000..987f73ccd
--- /dev/null
+++ b/test/regress/regress0/arith/CMakeLists.txt
@@ -0,0 +1 @@
+add_subdirectory(integers)
diff --git a/test/regress/regress0/arith/integers/CMakeLists.txt b/test/regress/regress0/arith/integers/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/arith/integers/CMakeLists.txt
diff --git a/test/regress/regress0/arrays/CMakeLists.txt b/test/regress/regress0/arrays/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/arrays/CMakeLists.txt
diff --git a/test/regress/regress0/aufbv/CMakeLists.txt b/test/regress/regress0/aufbv/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/aufbv/CMakeLists.txt
diff --git a/test/regress/regress0/auflia/CMakeLists.txt b/test/regress/regress0/auflia/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/auflia/CMakeLists.txt
diff --git a/test/regress/regress0/bv/CMakeLists.txt b/test/regress/regress0/bv/CMakeLists.txt
new file mode 100644
index 000000000..ad6d4787c
--- /dev/null
+++ b/test/regress/regress0/bv/CMakeLists.txt
@@ -0,0 +1 @@
+add_subdirectory(core)
diff --git a/test/regress/regress0/bv/core/CMakeLists.txt b/test/regress/regress0/bv/core/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/bv/core/CMakeLists.txt
diff --git a/test/regress/regress0/datatypes/CMakeLists.txt b/test/regress/regress0/datatypes/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/datatypes/CMakeLists.txt
diff --git a/test/regress/regress0/decision/CMakeLists.txt b/test/regress/regress0/decision/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/decision/CMakeLists.txt
diff --git a/test/regress/regress0/expect/CMakeLists.txt b/test/regress/regress0/expect/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/expect/CMakeLists.txt
diff --git a/test/regress/regress0/fmf/CMakeLists.txt b/test/regress/regress0/fmf/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/fmf/CMakeLists.txt
diff --git a/test/regress/regress0/lemmas/CMakeLists.txt b/test/regress/regress0/lemmas/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/lemmas/CMakeLists.txt
diff --git a/test/regress/regress0/nl/CMakeLists.txt b/test/regress/regress0/nl/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/nl/CMakeLists.txt
diff --git a/test/regress/regress0/parser/CMakeLists.txt b/test/regress/regress0/parser/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/parser/CMakeLists.txt
diff --git a/test/regress/regress0/precedence/CMakeLists.txt b/test/regress/regress0/precedence/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/precedence/CMakeLists.txt
diff --git a/test/regress/regress0/preprocess/CMakeLists.txt b/test/regress/regress0/preprocess/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/preprocess/CMakeLists.txt
diff --git a/test/regress/regress0/push-pop/CMakeLists.txt b/test/regress/regress0/push-pop/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/push-pop/CMakeLists.txt
diff --git a/test/regress/regress0/push-pop/arith/CMakeLists.txt b/test/regress/regress0/push-pop/arith/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/push-pop/arith/CMakeLists.txt
diff --git a/test/regress/regress0/push-pop/boolean/CMakeLists.txt b/test/regress/regress0/push-pop/boolean/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/push-pop/boolean/CMakeLists.txt
diff --git a/test/regress/regress0/quantifiers/CMakeLists.txt b/test/regress/regress0/quantifiers/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/quantifiers/CMakeLists.txt
diff --git a/test/regress/regress0/rels/CMakeLists.txt b/test/regress/regress0/rels/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/rels/CMakeLists.txt
diff --git a/test/regress/regress0/rewriterules/CMakeLists.txt b/test/regress/regress0/rewriterules/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/rewriterules/CMakeLists.txt
diff --git a/test/regress/regress0/sep/CMakeLists.txt b/test/regress/regress0/sep/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/sep/CMakeLists.txt
diff --git a/test/regress/regress0/sets/CMakeLists.txt b/test/regress/regress0/sets/CMakeLists.txt
new file mode 100644
index 000000000..0ccc8352e
--- /dev/null
+++ b/test/regress/regress0/sets/CMakeLists.txt
@@ -0,0 +1,6 @@
+add_subdirectory(feb3)
+add_subdirectory(jan24)
+add_subdirectory(jan27)
+add_subdirectory(jan28)
+add_subdirectory(jan30)
+add_subdirectory(mar2014)
diff --git a/test/regress/regress0/sets/feb3/CMakeLists.txt b/test/regress/regress0/sets/feb3/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/sets/feb3/CMakeLists.txt
diff --git a/test/regress/regress0/sets/jan24/CMakeLists.txt b/test/regress/regress0/sets/jan24/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/sets/jan24/CMakeLists.txt
diff --git a/test/regress/regress0/sets/jan27/CMakeLists.txt b/test/regress/regress0/sets/jan27/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/sets/jan27/CMakeLists.txt
diff --git a/test/regress/regress0/sets/jan28/CMakeLists.txt b/test/regress/regress0/sets/jan28/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/sets/jan28/CMakeLists.txt
diff --git a/test/regress/regress0/sets/jan30/CMakeLists.txt b/test/regress/regress0/sets/jan30/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/sets/jan30/CMakeLists.txt
diff --git a/test/regress/regress0/sets/mar2014/CMakeLists.txt b/test/regress/regress0/sets/mar2014/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/sets/mar2014/CMakeLists.txt
diff --git a/test/regress/regress0/strings/CMakeLists.txt b/test/regress/regress0/strings/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/strings/CMakeLists.txt
diff --git a/test/regress/regress0/sygus/CMakeLists.txt b/test/regress/regress0/sygus/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/sygus/CMakeLists.txt
diff --git a/test/regress/regress0/tptp/Axioms/CMakeLists.txt b/test/regress/regress0/tptp/Axioms/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/tptp/Axioms/CMakeLists.txt
diff --git a/test/regress/regress0/tptp/CMakeLists.txt b/test/regress/regress0/tptp/CMakeLists.txt
new file mode 100644
index 000000000..77739f587
--- /dev/null
+++ b/test/regress/regress0/tptp/CMakeLists.txt
@@ -0,0 +1 @@
+add_subdirectory(Axioms)
diff --git a/test/regress/regress0/uf/CMakeLists.txt b/test/regress/regress0/uf/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/uf/CMakeLists.txt
diff --git a/test/regress/regress0/uflia/CMakeLists.txt b/test/regress/regress0/uflia/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/uflia/CMakeLists.txt
diff --git a/test/regress/regress0/uflra/CMakeLists.txt b/test/regress/regress0/uflra/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/uflra/CMakeLists.txt
diff --git a/test/regress/regress0/unconstrained/CMakeLists.txt b/test/regress/regress0/unconstrained/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/unconstrained/CMakeLists.txt
diff --git a/test/regress/regress1/CMakeLists.txt b/test/regress/regress1/CMakeLists.txt
new file mode 100644
index 000000000..8742c4e41
--- /dev/null
+++ b/test/regress/regress1/CMakeLists.txt
@@ -0,0 +1,14 @@
+add_subdirectory(aufbv)
+add_subdirectory(auflia)
+add_subdirectory(bv)
+add_subdirectory(datatypes)
+add_subdirectory(decision)
+add_subdirectory(fmf)
+add_subdirectory(lemmas)
+add_subdirectory(nl)
+add_subdirectory(quantifiers)
+add_subdirectory(rewriterules)
+add_subdirectory(sep)
+add_subdirectory(sets)
+add_subdirectory(strings)
+add_subdirectory(sygus)
diff --git a/test/regress/regress1/aufbv/CMakeLists.txt b/test/regress/regress1/aufbv/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress1/aufbv/CMakeLists.txt
diff --git a/test/regress/regress1/auflia/CMakeLists.txt b/test/regress/regress1/auflia/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress1/auflia/CMakeLists.txt
diff --git a/test/regress/regress1/bv/CMakeLists.txt b/test/regress/regress1/bv/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress1/bv/CMakeLists.txt
diff --git a/test/regress/regress1/datatypes/CMakeLists.txt b/test/regress/regress1/datatypes/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress1/datatypes/CMakeLists.txt
diff --git a/test/regress/regress1/decision/CMakeLists.txt b/test/regress/regress1/decision/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress1/decision/CMakeLists.txt
diff --git a/test/regress/regress1/fmf/CMakeLists.txt b/test/regress/regress1/fmf/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress1/fmf/CMakeLists.txt
diff --git a/test/regress/regress1/lemmas/CMakeLists.txt b/test/regress/regress1/lemmas/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress1/lemmas/CMakeLists.txt
diff --git a/test/regress/regress1/nl/CMakeLists.txt b/test/regress/regress1/nl/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress1/nl/CMakeLists.txt
diff --git a/test/regress/regress1/quantifiers/CMakeLists.txt b/test/regress/regress1/quantifiers/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress1/quantifiers/CMakeLists.txt
diff --git a/test/regress/regress1/rewriterules/CMakeLists.txt b/test/regress/regress1/rewriterules/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress1/rewriterules/CMakeLists.txt
diff --git a/test/regress/regress1/sep/CMakeLists.txt b/test/regress/regress1/sep/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress1/sep/CMakeLists.txt
diff --git a/test/regress/regress1/sets/CMakeLists.txt b/test/regress/regress1/sets/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress1/sets/CMakeLists.txt
diff --git a/test/regress/regress1/strings/CMakeLists.txt b/test/regress/regress1/strings/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress1/strings/CMakeLists.txt
diff --git a/test/regress/regress1/sygus/CMakeLists.txt b/test/regress/regress1/sygus/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress1/sygus/CMakeLists.txt
diff --git a/test/regress/regress2/CMakeLists.txt b/test/regress/regress2/CMakeLists.txt
new file mode 100644
index 000000000..43ec0b68b
--- /dev/null
+++ b/test/regress/regress2/CMakeLists.txt
@@ -0,0 +1 @@
+add_subdirectory(arith)
diff --git a/test/regress/regress2/arith/CMakeLists.txt b/test/regress/regress2/arith/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress2/arith/CMakeLists.txt
diff --git a/test/regress/regress3/CMakeLists.txt b/test/regress/regress3/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress3/CMakeLists.txt
diff --git a/test/regress/regress4/CMakeLists.txt b/test/regress/regress4/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress4/CMakeLists.txt
diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/system/CMakeLists.txt
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
new file mode 100644
index 000000000..3e2dde59b
--- /dev/null
+++ b/test/unit/CMakeLists.txt
@@ -0,0 +1,7 @@
+add_subdirectory(context)
+add_subdirectory(expr)
+add_subdirectory(main)
+add_subdirectory(parser)
+add_subdirectory(prop)
+add_subdirectory(theory)
+add_subdirectory(util)
diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/unit/context/CMakeLists.txt
diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/unit/expr/CMakeLists.txt
diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/unit/main/CMakeLists.txt
diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/unit/parser/CMakeLists.txt
diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/unit/prop/CMakeLists.txt
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/unit/theory/CMakeLists.txt
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/unit/util/CMakeLists.txt