From 88fb54a554f1a374a380b1808d355f096437d1c0 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 5 Oct 2020 16:14:10 -0700
Subject: [PATCH] cmake: Add warning when unit testing is disabled due to
 assertions being disabled. (#5204)

This further fixes the testing instructions for API tests (formerly known as system tests)
in INSTALL.md.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
---
 CMakeLists.txt |  1 +
 INSTALL.md     | 25 ++++++++++++++-----------
 2 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 4b4b298ff..8eab22e4a 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -289,6 +289,7 @@ endif()
 # Only enable unit testing if assertions are enabled. Otherwise, unit tests
 # that expect AssertionException to be thrown will fail.
 if(NOT ENABLE_ASSERTIONS)
+  message(WARNING "Disabling unit tests since assertions are disabled.")
   set(ENABLE_UNIT_TESTING OFF)
 endif()
 
diff --git a/INSTALL.md b/INSTALL.md
index 7143dfc0e..b3308726b 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -229,8 +229,8 @@ We have 4 categories of tests:
   (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**)
+- **api tests** in directory `test/api`
+  (label: **api**)
 - **unit tests** in directory `test/unit`
   (label: **unit**)
 
@@ -238,26 +238,29 @@ We have 4 categories of 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>
+    make apitests                         # build and run all system tests
+    make <api_test>                       # build test/system/<system_test>.<ext>
+    ctest api/<api_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`)
+We use prefix `api/` + `<api_test>` (for `<api_test>` in `test/api`)
 as test target name.  
 
-    make ouroborous                       # build test/system/ouroborous.cpp
+    make ouroborous                       # build test/api/ouroborous.cpp
     ctest -R ouroborous                   # run all tests that match '*ouroborous*'
-                                          # > runs system/ouroborous
+                                          # > runs api/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
+                                          # > runs api/ouroborous
+    ctest -R api/ouroborous$              # run all tests that match '*api/ouroborous'
+                                          # > runs api/ouroborous
 ### Testing Unit Tests
 
 The unit tests are not built by default.
 
+Note that CVC4 can only be configured with unit tests in non-static builds with
+assertions enabled.
+
     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>
-- 
2.30.2