cmake: New INSTALL.md for build and testing instructions. (#2536)

3 files changed, 337 insertions, 273 deletions

diff --git a/INSTALL b/INSTALL
deleted file mode 100644
index 655c0e005..000000000
--- a/INSTALL
+++ /dev/null
@@ -1,259 +0,0 @@
-CVC4 prerelease version 1.7.
-
-** Quick-start instructions
-
-*** Supported operating systems
-
-CVC4 can be built on Linux and macOS.  For Windows, CVC4 can be cross-compiled
-using Mingw-w64.  We recommend a 64-bit operating system.
-
-On macOS, we recommend using Homebrew (https://brew.sh/) to install the
-dependencies.  We also have a Homebrew Tap available at
-https://github.com/CVC4/homebrew-cvc4 .
-
-*** Build dependencies
-
-The following tools and libraries are required to build and run CVC4.
-Versions given are minimum versions; more recent versions should be
-compatible.
-
-  GNU C and C++ (gcc and g++) or Clang, reasonably recent versions
-  GNU Make
-  GNU Bash
-  GMP v4.2 (GNU Multi-Precision arithmetic library)
-  libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library)
-  The Boost C++ base libraries
-
-Some features, such as the theory of floating-point numbers, require optional
-dependencies, please refer to the section "Optional dependencies" below for
-details.
-
-If "make" is non-GNU on your system, make sure to invoke "gmake" (or
-whatever GNU Make is installed as).  If your usual shell is not Bash,
-the configure script should auto-correct this.  If it does not, you'll
-see strange shell syntax errors, and you may need to explicitly set
-SHELL or CONFIG_SHELL to the location of bash on your system.
-
-*** Installing libantlr3c: ANTLR parser generator C support library
-
-For libantlr3c, you can use the convenience script in
-contrib/get-antlr-3.4.  This will download, patch, and install
-libantlr3c.  On a 32-bit machine, or if you have difficulty building
-libantlr3c (or difficulty getting CVC4 to link against it later), you
-may need to remove the --enable-64bit part in the script.  (If you're
-curious, the manual instructions are at
-http://cvc4.cs.stanford.edu/wiki/Developer%27s_Guide#ANTLR3 .)
-
-*** Installing the Boost C++ base libraries
-
-A Boost package is available on most Linux distributions and Homebrew; check
-yours for a package named something like libboost-dev or boost-devel.  There
-are a number of additional Boost packages in some distributions, but this
-"basic" one should be sufficient for building CVC4.
-
-Should you want to install Boost manually, or to learn more about the
-Boost project, please visit http://www.boost.org/.
-
-*** Optional dependencies
-
-None of these is required, but can improve CVC4 as described below:
-
-  Optional: SymFPU (an implementation of SMT-LIB/IEEE-754 floating-point
-            operations in terms of bit-vector operations)
-  Optional: CaDiCaL (optional SAT solver)
-  Optional: CryptoMiniSat (optional SAT solver)
-  Optional: LFSC (the LFSC proof checker)
-  Optional: SWIG 3.0.x (Simplified Wrapper and Interface Generator)
-  Optional: CLN v1.3 or newer (Class Library for Numbers)
-  Optional: glpk-cut-log (A fork of the GNU Linear Programming Kit)
-  Optional: ABC library (for improved bitvector support)
-  Optional: GNU Readline library (for an improved interactive experience)
-  Optional: The Boost C++ threading library (libboost_thread)
-  Optional: CxxTest unit testing framework
-
-SymFPU is required for supporting the theory of floating-point numbers.  It can
-be installed using the contrib/get-symfpu script.  Use --with-symfpu when
-configuring CVC4 to build with the dependency.
-
-CaDiCaL is a SAT solver that can be used for solving non-incremental bit-vector
-problems when using eager bit-blasting.  This dependency may improve
-performance. It can be installed using the contrib/get-cadical script.  Use
---with-cadical when configuring CVC4 to build with this dependency.
-
-CryptoMiniSat is a SAT solver that can be used for solving bit-vector problems
-when using eager bit-blasting.  This dependency may improve performance. It can
-be installed using the contrib/get-cryptominisat script.  Use
---with-cryptominisat when configuring CVC4 to build with this dependency.
-
-LFSC is required to check proofs internally with --check-proofs. It can be
-installed using the contrib/get-lfsc script.  Use --with-lfsc when configuring
-CVC4 to build with this dependency.
-
-SWIG is necessary to build the Java API (and of course a JDK is
-necessary, too).  SWIG 1.x/2.x won't work; you'll need 3.0, and the more
-recent the better.  See "Language bindings" below for build instructions.
-
-CLN is an alternative multiprecision arithmetic package that can offer
-better performance and memory footprint than GMP.  CLN is covered by
-the GNU General Public License, version 3; so if you choose to use
-CVC4 with CLN support, you are licensing CVC4 under that same license.
-(Usually CVC4's license is more permissive than GPL is; see the file
-COPYING in the CVC4 source distribution for details.)  Please visit
-http://www.ginac.de/CLN/ for more details about CLN.
-
-glpk-cut-log is a fork of GLPK (the GNU Linear Programming Kit).
-This can be used to speed up certain classes of problems for the arithmetic
-implementation in CVC4. (This is not recommended for most users.) The source
-code for glpk-cut-log is available at:
-https://github.com/timothy-king/glpk-cut-log/
-The only option for installation of glpk-cut-log is downloading the library,
-compiling and installing it manually.  CVC4 is no longer compatible with the
-main GLPK library. GLPK and glpk-cut-log are covered by the GNU General Public
-License, version 3; so if you choose to use CVC4 with GLPK support, you are
-licensing CVC4 under that same license.
-(Usually CVC4's license is more permissive; see above discussion.)
-Please visit http://www.gnu.org/software/glpk/ for more details about GLPK.
-
-ABC: A System for Sequential Synthesis and Verification is a library
-for synthesis and verification of logic circuits. This can be used to
-speed up the eager bit-vector solver by first encoding the bit-blasted
-formula into AIG format and then using ABC to simplify the AIG. To
-install abc run the contrib/get-abc script which will download and
-install a compatible version of ABC in the cvc4 directory. To configure
-CVC4 to use abc configure with --with-abc and --with-abc-dir=PATH, where
-PATH corresponds to the install path of ABC. To run CVC4 using ABC use
-the --bitblast-aig command line argument.
-Please visit http://www.eecs.berkeley.edu/~alanmi/abc/ for more details
-on ABC.
-
-The GNU Readline library is optionally used to provide command
-editing, tab completion, and history functionality at the CVC prompt
-(when running in interactive mode).  Check your distribution for a
-package named "libreadline-dev" or "readline-devel" or similar.  This
-library is covered by the GNU General Public License, version 3.  Like
-the above-mentioned libraries, if you choose to use CVC4 with readline
-support, you are licensing CVC4 under that same license.  (Please visit
-http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html for more
-details about readline.)
-
-The Boost C++ threading library (often packaged independently of the
-Boost base library) is needed to run CVC4 in "portfolio"
-(multithreaded) mode.  Check your distribution for a package named
-"libboost-thread-dev" or similar.
-
-CxxTest is necessary to run CVC4's unit tests (included with the
-distribution).  Running these is not really required for users of
-CVC4; "make check" will skip unit tests if CxxTest isn't available,
-and go on to run the extensive system- and regression-tests in the
-source tree.  However, if you're interested, you can download CxxTest
-at http://cxxtest.com/ .
-
-*** Building CVC4
-
-Once the build dependencies are satisfied, you should be able to configure,
-make, make check, and make install without incident:
-
-    ./autogen.sh  [not required when building from a source distribution]
-    ./configure   [use --prefix to specify a prefix; default /usr/local
-                   use --with-* to use optional dependencies]
-    make
-    make check    [optional but a good idea!]
-
-To build from a repository checkout (rather than a distributed CVC4
-tarball), there are additional dependencies; see below.
-
-You can then "make install" to install in the prefix you gave to
-the configure script (/usr/local by default).  ** You should run
-"make check" ** before installation to ensure that CVC4 has been
-built correctly.  In particular, GCC version 4.5.1 seems to have a
-bug in the optimizer that results in incorrect behavior (and wrong
-results) in many builds.  This is a known problem for MiniSat, and
-since MiniSat is at the core of CVC4, a problem for CVC4.  "make check"
-easily detects this problem (by showing a number of FAILed test cases).
-It is ok if the unit tests aren't run as part of "make check", but all
-system tests and regression tests should pass without incident.
-
-To build API documentation, use "make doc".  Documentation is produced
-under doc/ but is not installed by "make install".
-
-Examples and tutorials are not installed with "make install."  You may
-want to "make install-examples".  See below.
-
-For more information about the build system itself (probably not
-necessary for casual users), see the Appendix at the bottom of this
-file.
-
-*** Language bindings
-
-There are several options available for using CVC4 from the API.
-
-First, CVC4 offers a complete and flexible API for manipulating
-expressions, maintaining a stack of assertions, and checking
-satisfiability, and related things.  The C++ libraries (libcvc4.so and
-libcvc4parser.so) and required headers are installed normally via a
-"make install".  This API is also available from Java (via CVC4.jar
-and libcvc4jni.so) by configuring with --enable-language-bindings=java.
-You'll also need SWIG 2.0 installed (and you might need to help
-configure find it if you installed it in a nonstandard place with
---with-swig-dir=/path/to/swig/installation).  You may also need to
-give the configure script the path to your Java headers (in
-particular, jni.h).  You might do so with (for example):
-
-  ./configure --enable-language-bindings=java \
-      JAVA_CPPFLAGS=-I/usr/lib/jvm/java-6-openjdk-amd64/include
-
-The examples/ directory includes some basic examples (the "simple vc" family of
-examples) of all these interfaces.
-
-In principle, since we use SWIG to generate the native Java API, we
-could support other languages as well.  However, using CVC4 from other
-languages is not supported, nor expected to work, at this time.  If
-you're interested in helping to develop, maintain, and test a language
-binding, please contact one of the project leaders.
-
-*** Building CVC4 from a repository checkout
-
-CVC4's main repository is kept on GitHub at:
-
-  https://github.com/CVC4/CVC4
-
-and there are numerous experimental forks housed on GitHub as well,
-by different developers, implementing various features.
-
-The following tools and libraries are additionally required to build
-CVC4 from from a repository checkout rather than from a prepared
-source tarball.
-
-  Automake v1.11 or later
-  Autoconf v2.61 or later
-  Libtool v2.2 or later
-  ANTLR3 v3.2 or v3.4 
-  Python (2.x or 3.x)
-
-First, use "./autogen.sh" to create the configure script.  Then proceed as
-normal for any distribution tarball.  The parsers are pre-generated for the
-tarballs, but don't exist in the repository; hence the extra ANTLR3 requirement
-to generate the source code for the parsers, when building from the repository.
-Similarly, Python is required for generating some of the code.
-
-*** Examples and tutorials are not built or installed
-
-Examples are not built by "make" or "make install".  See
-examples/README for information on what to find in the examples/
-directory, as well as information about building and installing them.
-
-*** Appendix: Build architecture
-
-The build system is generated by automake, libtool, and autoconf.  It
-is somewhat nonstandard, though, which (for one thing) requires that
-GNU Make be used.  If you ./configure in the top-level source
-directory, the objects will actually all appear in
-builds/${arch}/${build_id}.  This is to allow multiple, separate
-builds in the same place (e.g., an assertions-enabled debugging build
-alongside a production build), without changing directories at the
-shell.  The "current" build is maintained until you re-configure.
-
-You can also create your own build directory inside or outside of the
-source tree and configure from there.  All objects will then be built
-in that directory, and you'll ultimately find the "cvc4" binary in
-src/main/, and the libraries under src/ and src/parser/.
diff --git a/INSTALL.md b/INSTALL.md
new file mode 100644
index 000000000..2f0c7a051
--- /dev/null
+++ b/INSTALL.md
@@ -0,0 +1,325 @@
+CVC4 prerelease version 1.7.
+============================
+
+## Supported Operating Systems
+
+CVC4 can be built on Linux and macOS.  For Windows, CVC4 can be cross-compiled
+using Mingw-w64.  We recommend a 64-bit operating system.
+
+On macOS, we recommend using Homebrew (https://brew.sh/) to install the
+dependencies.  We also have a Homebrew Tap available at
+https://github.com/CVC4/homebrew-cvc4 .
+
+## Build dependencies
+
+The following tools and libraries are required to build and run CVC4.  
+Versions given are minimum versions; more recent versions should be
+compatible.
+
+- [GNU C and C++ (gcc and g++)](https://gcc.gnu.org)
+  or [Clang](https://clang.llvm.org) (reasonably recent versions)
+- [CMake >= 3.1](https://cmake.org)
+- [GNU Bash](https://www.gnu.org/software/bash/)
+- [Python >= 2.7](https://www.python.org)
+- [GMP v4.2 (GNU Multi-Precision arithmetic library)](https://gmplib.org)
+- [libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library)](http://www.antlr3.org/)
+
+Some features, such as the theory of floating-point numbers, require
+[optional dependencies](optional-dependencies) (see below).
+
+### Installing libantlr3c: ANTLR parser generator C support library
+
+For libantlr3c, you can use the script contrib/get-antlr-3.4.
+This will download, patch, and install libantlr3c.
+
+If you're on a 32-bit machine, or if you have difficulty building
+libantlr3c (or difficulty getting CVC4 to link against it), you
+may need to remove the configure option `--enable-64bit` in the script.
+
+### Warning: GCC 4.5.1
+
+GCC version 4.5.1 seems to have a bug in the optimizer that may result in
+incorrect behavior (and wrong results) in many builds. This is a known problem
+for MiniSat, and since MiniSat is at the core of CVC4, a problem for CVC4.
+We recommend using a GCC version > 4.5.1.
+
+## Optional Dependencies
+
+### SymFPU (Support for the Theory of Floating Point Numbers)
+
+[SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4)
+is an implementation of SMT-LIB/IEEE-754 floating-point operations in terms
+of bit-vector operations.
+It is required for supporting the theory of floating-point numbers and
+can be installed using the `contrib/get-symfpu` script.  
+Configure CVC4 with `configure.sh --symfpu` to build with this dependency.
+
+### CaDiCaL (Optional SAT solver)
+
+[CaDiCaL](https://github.com/arminbiere/cadical)
+is a SAT solver that can be used for solving non-incremental bit-vector
+problems with eager bit-blasting. This dependency may improve performance.
+It can be installed using the `contrib/get-cadical script`.  
+Configure CVC4 with `configure.sh --cadical` to build with this dependency.
+
+### CryptoMiniSat (Optional SAT solver)
+
+[CryptoMinisat](https://github.com/msoos/cryptominisat)
+is a SAT solver that can be used for solving bit-vector problems with eager
+bit-blasting. This dependency may improve performance.
+It can be installed using the `contrib/get-cryptominisat` script.  
+Configure CVC4 with `configure.sh --cryptominisat` to build with this
+dependency.
+
+### LFSC (The LFSC Proof Checker)
+
+[LFSC](https://github.com/CVC4/LFSC) is required to check proofs internally
+with --check-proofs. It can be installed using the `contrib/get-lfsc` script.  
+Configure CVC4 with `configure.sh --lfsc` to build with this dependency.
+
+### SWIG >= 3.0.x (Simplified Wrapper and Interface Generator)
+
+SWIG 3.0.x (and a JDK) is necessary to build the Java API.
+See [Language Bindings](language-bindings) below for build instructions.
+
+### CLN >= v1.3 (Class Library for Numbers)
+
+[CLN](http://www.ginac.de/CLN)
+is an alternative multiprecision arithmetic package that may offer better
+performance and memory footprint than GMP.  
+Configure CVC4 with `configure.sh --cln` to build with this dependency.
+
+Note that CLN is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html).
+If you choose to use CVC4 with CLN support, you are licensing CVC4 under that
+same license.
+(Usually CVC4's license is more permissive than GPL, see the file `COPYING` in
+the CVC4 source distribution for details.)
+
+### glpk-cut-log (A fork of the GNU Linear Programming Kit)
+
+[glpk-cut-log](https://github.com/timothy-king/glpk-cut-log/) is a fork of
+[GLPK](http://www.gnu.org/software/glpk/) (the GNU Linear Programming Kit).
+This can be used to speed up certain classes of problems for the arithmetic
+implementation in CVC4. (This is not recommended for most users.)
+
+glpk-cut-log can be installed using the `contrib/get-glpk-cut-log` script.
+Note that the only installation option is manual installation via this script.
+CVC4 is no longer compatible with the main GLPK library.  
+Configure CVC4 with `configure.sh --glpk` to build with this dependency.
+
+Note that GLPK and glpk-cut-log are covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html).
+If you choose to use CVC4 with GLPK support, you are licensing CVC4 under that
+same license.
+(Usually CVC4's license is more permissive; see above discussion.)
+
+### ABC library (Improved Bit-Vector Support)
+
+[ABC](http://www.eecs.berkeley.edu/~alanmi/abc/) (A System for Sequential
+Synthesis and Verification) is a library for synthesis and verification of
+logic circuits. This dependency may improve performance of the eager
+bit-vector solver. When enabled, the bit-blasted formula is encoded into
+and-inverter-graphs (AIG) and ABC is used to simplify these AIGs.
+
+ABC can be installed using the `contrib/get-abc` script.  
+Configure CVC4 with `configure.sh --abc` to build with this dependency.
+
+### GNU Readline library (Improved Interactive Experience)
+
+The [GNU Readline](http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html)
+library is optionally used to provide command editing, tab completion, and
+history functionality at the CVC4 prompt (when running in interactive mode).
+Check your distribution for a package named "libreadline-dev" or
+"readline-devel" or similar.
+
+Note that GNU Readline is covered by the [GNU General Public License, version 3](https://www.gnu.org/licenses/gpl-3.0.en.html).
+If you choose to use CVC4 with GNU Readline support, you are licensing CVC4
+under that same license.
+(Usually CVC4's license is more permissive; see above discussion.)
+
+### libboost_thread: The Boost C++ threading library (Portfolio Builds)
+
+The [Boost](http://www.boost.org) C++ threading library (often packaged
+independently of the Boost base library) is needed to run CVC4 in "portfolio"
+(multithreaded) mode.
+Check your distribution for a package named "libboost-thread-dev" or similar.
+
+### Boost C++ base libraries (Examples)
+
+The [Boost](http://www.boost.org) C++ base library is needed for some examples
+provided with CVC4.
+
+### CxxTest Unit Testing Framework (Unit Tests)
+
+[CxxTest](http://cxxtest.com) is required to optionally run CVC4's unit tests
+(included with the distribution). See [Testing](testing) below for more details.
+
+
+## Building CVC4
+
+    ./configure.sh   # use --prefix to specify a prefix (default: /usr/local)
+                     # use --name=<PATH> for custom build directory
+    cd <build_dir>   # default is ./build
+    make             # use -jN for parallel build with N threads
+    make check       # to run default set of tests
+    make install     # to install into the prefix specified above
+
+All binaries are built into `<build_dir>/bin`, the CVC4 library is built into
+`<build_dir>/src`.
+
+## Language bindings
+
+CVC4 provides a complete and flexible C++ API (see `examples/api` for examples).
+It further provides Java (see `examples/SimpleVC.java` and `examples/api/java`)
+and Python (see `examples/SimpleVC.py`) API bindings.
+
+Configure CVC4 with `configure.sh --language-bindings=[java,python,all]`
+to build with language bindings.  
+Note that this requires SWIG >= 3.0.x.
+
+In principle, since we use SWIG to generate the native Java and PythonAPI,
+we could support other languages as well. However, using CVC4 from other
+languages is not supported, nor expected to work, at this time.
+If you're interested in helping to develop, maintain, and test a language
+binding, please contact one of the project leaders.
+
+## Building the Examples
+
+The examples provided in directory `examples` are not built by default.
+
+    make examples                      # build all examples
+    make runexamples                   # build and run all examples
+    make <example>                     # build examples/<subdir>/<example>.<ext>
+    ctest example/<subdir>/<example>   # run test example/<subdir>/<example>
+
+All examples binaries are built into `<build_dir>/bin/examples`.
+
+See `examples/README` for more detailed information on what to find in the
+`examples` directory.
+
+## Testing CVC4
+
+We use `ctest` as test infrastructure, for all command-line options of ctest,
+see `ctest -h`. Some useful options are:
+
+    ctest -R <regex>           # run all tests with names matching <regex>
+    ctest -E <regex>           # exclude tests with names matching <regex>
+    ctest -L <regex>           # run all tests with labels matching <regex>
+    ctest -LE <regex>          # exclude tests with labels matching <regex>
+    ctest                      # run all tests
+    ctest -jN                  # run all tests in parallel with N threads
+    ctest --output-on-failure  # run all tests and print output of failed tests
+
+We have 4 categories of tests:
+- **examples** in directory `examples`
+  (label: **example**)
+- **regression tests** (5 levels) in directory `test/regress`
+  (label: **regressN** with N the regression level)
+- **system tests** in directory `test/system`
+  (label: **system**)
+- **unit tests** in directory `test/unit`
+  (label: **unit**)
+
+### Testing Examples
+
+For building instructions, see [Building the Examples](building-the-examples).
+
+We use prefix `example/` + `<subdir>/` + `<example>` (for `<example>` in
+`example/<subdir>/`) as test target name.  
+
+    make bitvectors                       # build example/api/bitvectors.cpp
+    ctest -R bitvectors                   # run all tests that match '*bitvectors*'
+                                          # > runs example/api/bitvectors
+                                          # >      example/api/bitvectors_and_arrays
+                                          # >      ...
+    ctest -R bitvectors$                  # run all tests that match '*bitvectors'
+                                          # > runs example/api/bitvectors
+    ctest -R example/api/bitvectors$      # run all tests that match '*example/api/bitvectors'
+                                          # > runs example/api/bitvectors
+
+
+### Testing System Tests
+
+The system tests are not built by default.
+
+    make systemtests                      # build and run all system tests
+    make <system_test>                    # build test/system/<system_test>.<ext>
+    ctest system/<system_test>            # run test/system/<system_test>.<ext>
+
+All system test binaries are built into `<build_dir>/bin/test/system`.
+
+We use prefix `system/` + `<system_test>` (for `<system_test>` in `test/system`)
+as test target name.  
+
+    make ouroborous                       # build test/system/ouroborous.cpp
+    ctest -R ouroborous                   # run all tests that match '*ouroborous*'
+                                          # > runs system/ouroborous
+    ctest -R ouroborous$                  # run all tests that match '*ouroborous'
+                                          # > runs system/ouroborous
+    ctest -R system/ouroborous$           # run all tests that match '*system/ouroborous'
+                                          # > runs system/ouroborous
+### Testing Unit Tests
+
+The unit tests are not built by default.
+
+    make units                            # build and run all unit tests
+    make <unit_test>                      # build test/unit/<subdir>/<unit_test>.<ext>
+    ctest unit/<subdir>/<unit_test>       # run test/unit/<subdir>/<unit_test>.<ext>
+
+All unit test binaries are built into `<build_dir>/bin/test/unit`.
+
+We use prefix `unit/` + `<subdir>/` + `<unit_test>` (for `<unit_test>` in
+`test/unit/<subdir>`) as test target name.  
+
+    make map_util_black                   # build test/unit/base/map_util_black.cpp
+    ctest -R map_util_black               # run all tests that match '*map_util_black*'
+                                          # > runs unit/base/map_util_black
+    ctest -R base/map_util_black$         # run all tests that match '*base/map_util_black'
+                                          # > runs unit/base/map_util_black
+    ctest -R unit/base/map_util_black$    # run all tests that match '*unit/base/map_util_black'
+                                          # > runs unit/base/map_util_black
+
+### Testing Regression Tests
+
+We use prefix `regressN/` + `<subdir>/` + `<regress_test>` (for `<regress_test>`
+in level `N` in `test/regress/regressN/<subdir>`) as test target name.  
+
+    ctest -L regress                      # run all regression tests
+    ctest -L regress0                     # run all regression tests in level 0
+    ctest -L regress[0-1]                 # run all regression tests in level 0 and 1
+    ctest -R regress                      # run all regression tests
+    ctest -R regress0                     # run all regression tests in level 0
+    ctest -R regress[0-1]                 # run all regression tests in level 0 and 1
+    ctest -R regress0/bug288b             # run all tests that match '*regress0/bug288b*'
+                                          # > runs regress0/bug288b
+### Custom Targets
+
+All custom test targets build and run a preconfigured set of tests.
+
+- `make check [-jN] [ARGS=-jN]`  
+  The default build-and-test target for CVC4, builds and runs all examples,
+  all system and unit tests, and regression tests from levels 0 and 1.
+
+- `make systemtests [-jN] [ARGS=-jN]`  
+  Build and run all system tests.
+
+- `make units [-jN] [ARGS=-jN]`  
+  Build and run all unit tests.
+
+- `make regress [-jN] [ARGS=-jN]`  
+  Build and run all regression tests.
+
+- `make runexamples [-jN] [ARGS=-jN]`  
+  Build and run all examples.
+
+- `make coverage [-jN] [ARGS=-jN]`  
+  Build and run all tests (system and unit tests, regression tests level 0-4)
+  with gcov to determine code coverage.
+
+We use `ctest` as test infrastructure, and by default all test targets
+are configured to **run** in parallel with the maximum number of threads
+available on the system. Override with `ARGS=-jN`.
+
+Use `-jN` for parallel **building** with `N` threads.
+
+
+
diff --git a/examples/README b/examples/README
index df8cffe73..cc3c23f26 100644
--- a/examples/README
+++ b/examples/README
@@ -1,8 +1,11 @@
+Examples
+--------
+
 This directory contains usage examples of CVC4's different language
 bindings, library APIs, and also tutorial examples from the tutorials
 available at http://cvc4.cs.stanford.edu/wiki/Tutorials
 
-*** Files named SimpleVC*, simple_vc*
+### SimpleVC*, simple_vc*
 
 These are examples of how to use CVC4 with each of its library
 interfaces (APIs) and language bindings.  They are essentially "hello
@@ -10,24 +13,19 @@ world" examples, and do not fully demonstrate the interfaces, but
 function as a starting point to using simple expressions and solving
 functionality through each library.
 
-*** Targeted examples
+### Targeted examples
 
 The "api" directory contains some more specifically-targeted
 examples (for bitvectors, for arithmetic, etc.).  The "api/java"
 directory contains the same examples in Java.
 
-*** Installing example source code
-
-Examples are not automatically installed by "make install".  If you
-wish to install them, use "make install-examples" after you configure
-your CVC4 source tree.  They'll appear in your documentation
-directory, under the "examples" subdirectory (so, by default,
-in /usr/local/share/doc/cvc4/examples).
+### Building Examples
 
-*** Building examples
+The examples provided in this directory are not built by default.
 
-Examples can be built as a separate step, after building CVC4 from
-source.  After building CVC4, you can run "make examples".  You'll
-find the built binaries in builds/examples (or just in "examples" if
-you configured a build directory outside of the source tree).
+    make examples                      # build all examples
+    make runexamples                   # build and run all examples
+    make <example>                     # build examples/<subdir>/<example>.<ext>
+    ctest example//<subdir>/<example>  # run examples/<subdir>/<example>.<ext>
 
+The examples binaries are built into `<build_dir>/bin/examples`.