Add regression test information to COMPILING.md

This adds information on how to run regression tests
using bnoth cmake and make to COMPILING.md.
Also ensures COMPILING.md follows clang-format-7.

Author: TGWDB

COMPILING.md

@@ -1,4 +1,4 @@
-# WHAT ARCHITECTURE?
+#WHAT ARCHITECTURE ?
 
 CPROVER now needs a C++11 compliant compiler and is known to work in the
 following environments:
@@ -18,7 +18,7 @@ past, but are not actively tested:
 - Solaris 11
 - FreeBSD 11
 
-# Building using CMake
+#Building using CMake
 
 Building with CMake is supported across Linux, MacOS X and Windows with Visual
 Studio 2019. There are also hand-written make files which can be used to build
@@ -118,7 +118,7 @@ files.
    complete set of built binaries can be found in `./build/bin` once the build
    is complete.
 
-# Building using hand-written make files.
+#Building using hand - written make files.
 
 The rest of this section is split up based on the platform being built on. 
 Please read the section appropriate for your machine.
@@ -253,7 +253,7 @@ Maven 3 manually.
    gmake -C jbmc/src
    ```
 
-# WORKING WITH ECLIPSE
+#WORKING WITH ECLIPSE
 
 To work with Eclipse, do the following:
 
@@ -270,7 +270,7 @@ the need to integrate JBMC as a separate project. Be aware that you need to
 change the build location (Select project in Eclipse -> Properties -> C/C++ 
 Build) to one of the src directories.
 
-# WORKING WITH DOCKER
+#WORKING WITH DOCKER
 
 To compile and run the tools in a Docker container, do the following:
 
@@ -284,9 +284,9 @@ To compile and run the tools in a Docker container, do the following:
    that contains the tests to the container. A possible invocation that does that
    is: `$ docker run --mount type=bind,source=local/path/with/files,target=/mnt/analysis -i t cbmc`. In the
    resulting container, the files present in the local file system under
-   `local/path/with/files` will be present under `/mnt/analysis`. 
+   `local/path/with/files` will be present under `/mnt/analysis`.
 
-# OPTIONS AND VARIABLES
+#OPTIONS AND VARIABLES
 
 ## Compiling with CUDD
 
@@ -482,3 +482,42 @@ successfully on Windows or macOS.
    The argument for the IPASIR parameter gives the build system the location for
    the IPASIR headers, which is needed for the cbmc includes of `ipasir.h`. The
    compiled binary will be placed in `cbmc/src/cbmc/cbmc`.
+This document assumes you have already been able to build CPROVER on
+your chosen architecture. For details on building CPROVER see
+COMPILING.md.
+
+#RUNNING REGRESSION TESTS
+
+Regression tests can be run using cmake or make. Your choice here
+should be the same as the compiling of the project itself.
+
+Note that running all regression tests can be slow when a debug
+build of CPROVER is used.
+
+## CMAKE
+
+This can be done by changing to the directory you built the
+project in with cmake and running ctest as follows.
+```
+cd <build_dir>
+ctest . -V -L CORE
+```
+You can also specify a pattern of tests to run as follows.
+```
+ctest . -V -L CORE -R <pattern>
+```
+For example
+```
+ctest . -V -L CORE -R goto
+```
+that will run all CORE tests that include `goto` in their
+name.
+
+## MAKE
+
+This can be done by changing to the regression directory and
+simply running make as follows.
+```
+cd regression
+make
+```