fixes to regression docs (#2679)

diff --git a/INSTALL.md b/INSTALL.md
index 98cef20618686c0ee03a4f27c9b6dd7f45df8a29..dc0de6cb4374ce0cccd5c9be9d5532455707028b 100644 (file)
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -151,7 +151,8 @@ 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.
+(included with the distribution). 
+See [Testing CVC4](#Testing-CVC4) below for more details.
 
 
 ## Building CVC4

diff --git a/test/regress/README.md b/test/regress/README.md
index d43ebf3379ebd3f4911dd68386e3c921191a53d9..28ccfb96b89d2027023effa911cd9d1e8d0a8d25 100644 (file)
--- a/test/regress/README.md
+++ b/test/regress/README.md
@@ -3,20 +3,10 @@
 ## Regression Levels and Running Regression Tests
 
 CVC4's regression tests are divided into 5 levels (level 0 to 4). Higher
-regression levels are reserved for longer running regressions. To run
-regressions up to a certain level use `make regressX` where `X` designates the
-level. `make regress` by default runs levels 0 and 1. On Travis, we only run
-regression level 0 to keep the time short. During our nightly builds, we run
-regression level 2.
+regression levels are reserved for longer running regressions. 
 
-To only run some benchmarks, you can use the `TEST_REGEX` environment variable.
-For example:
-
-```
-TEST_REGEX=quantifiers make regress0
-```
-
-This runs regression tests from level 0 that have "quantifiers" in their name.
+For running regressions tests, 
+see the [INSTALL](https://github.com/CVC4/CVC4/blob/master/INSTALL.md#testing-cvc4) file.
 
 By default, each invocation of CVC4 is done with a 10 minute timeout. To use a
 different timeout, set the `TEST_TIMEOUT` environment variable:
@@ -35,10 +25,10 @@ To add a new regression file, add the file to git, for example:
 git add regress/regress0/testMyFunctionality.cvc
 ```
 
-Also add it to [Makefile.tests](Makefile.tests) in this directory.
+Also add it to [CMakeLists.txt](CMakeLists.txt) in this directory.
 
 A number of regressions exist under test/regress that are not listed in
-[Makefile.tests](Makefile.tests). These are regressions that may someday be
+[CMakeLists.txt](CMakeLists.txt). These are regressions that may someday be
 included in the standard suite of tests, but are not yet included (perhaps they
 test functionality not yet supported).