--- /dev/null
+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)
+
--- /dev/null
+# 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)
--- /dev/null
+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)
--- /dev/null
+add_subdirectory(compat)
--- /dev/null
+add_subdirectory(c)
+add_subdirectory(java)
--- /dev/null
+add_subdirectory(cvc)
+add_subdirectory(smt1)
+add_subdirectory(smt2)
+add_subdirectory(tptp)
--- /dev/null
+add_subdirectory(bvminisat)
+add_subdirectory(minisat)
--- /dev/null
+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)
--- /dev/null
+add_subdirectory(java)
+add_subdirectory(regress)
+add_subdirectory(system)
+add_subdirectory(unit)
--- /dev/null
+add_subdirectory(regress0)
+add_subdirectory(regress1)
+add_subdirectory(regress2)
+add_subdirectory(regress3)
+add_subdirectory(regress4)
--- /dev/null
+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)
--- /dev/null
+add_subdirectory(integers)
--- /dev/null
+add_subdirectory(core)
--- /dev/null
+add_subdirectory(feb3)
+add_subdirectory(jan24)
+add_subdirectory(jan27)
+add_subdirectory(jan28)
+add_subdirectory(jan30)
+add_subdirectory(mar2014)
--- /dev/null
+add_subdirectory(Axioms)
--- /dev/null
+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)
--- /dev/null
+add_subdirectory(arith)
--- /dev/null
+add_subdirectory(context)
+add_subdirectory(expr)
+add_subdirectory(main)
+add_subdirectory(parser)
+add_subdirectory(prop)
+add_subdirectory(theory)
+add_subdirectory(util)