Always enable API black box unit tests (#7696)

Currently, when assertions are disabled, we do not enable any unit
tests. However, we have decided that it would be beneficial to do black
box unit testing of the API even when building cvc5 without assertions,
because the API is user facing. This commit makes the following changes:

- Always enables API black box unit tests
- Adds a test to check whether a buggy version of Clang is being used,
  which prevents the use of `-fno-access-control` for white box tests
- Fixes a spooky variable name in a Python unit test

6 files changed, 72 insertions, 55 deletions

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index f28309652..723752eb8 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -19,7 +19,7 @@ jobs:
 
           - name: macos:production
             os: macos-11
-            config: production --auto-download --all-bindings --editline
+            config: production --auto-download --python-bindings --editline
             cache-key: production
             python-bindings: true
             check-examples: true
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 9e70f4c3d..6adb6241e 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -251,10 +251,22 @@ endif()
 # https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling
 set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR};${PROJECT_SOURCE_DIR}/deps/install/lib")
 
-# Set visibility to default if unit tests are enabled
+# Set visibility to default if unit tests are enabled. If unit tests are
+# enabled, we also check if we can execute white box unit tests (some versions
+# of Clang have issues with the required flag).
+set(ENABLE_WHITEBOX_UNIT_TESTING OFF)
 if(ENABLE_UNIT_TESTING)
   set(CMAKE_CXX_VISIBILITY_PRESET default)
   set(CMAKE_VISIBILITY_INLINES_HIDDEN 0)
+
+  # Check if Clang version has the bug that was fixed in
+  # https://reviews.llvm.org/D93104
+  set(ENABLE_WHITEBOX_UNIT_TESTING ON)
+  check_cxx_compiler_flag("-faccess-control" HAVE_CXX_FLAGfaccess_control)
+  if(NOT HAVE_CXX_FLAGfaccess_control)
+    set(ENABLE_WHITEBOX_UNIT_TESTING OFF)
+    message(STATUS "Disabling white box unit tests")
+  endif()
 endif()
 
 #-----------------------------------------------------------------------------#
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index 3108582d9..feafc418a 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -38,7 +38,4 @@ add_custom_target(check
 add_subdirectory(regress)
 add_subdirectory(api EXCLUDE_FROM_ALL)
 add_subdirectory(binary EXCLUDE_FROM_ALL)
-
-if(ENABLE_UNIT_TESTING)
-  add_subdirectory(unit EXCLUDE_FROM_ALL)
-endif()
+add_subdirectory(unit EXCLUDE_FROM_ALL)
diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt
index c9e00213a..e58ada545 100644
--- a/test/api/python/CMakeLists.txt
+++ b/test/api/python/CMakeLists.txt
@@ -24,8 +24,8 @@ macro(cvc5_add_python_api_test name filename)
     # directory for importing the python bindings
     WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python)
     set_tests_properties(${test_name} 
-	    PROPERTIES LABELS "api"
-	    ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH}:${CMAKE_SOURCE_DIR}/api/python)
+      PROPERTIES LABELS "api"
+      ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH}:${CMAKE_SOURCE_DIR}/api/python)
 endmacro()
 
 # add specific test files
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 9be9dcefa..725827abe 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -36,48 +36,52 @@ set(CVC5_UNIT_TEST_FLAGS_BLACK
 
 # Generate and add unit test.
 macro(cvc5_add_unit_test is_white name output_dir)
-  set(test_src ${CMAKE_CURRENT_LIST_DIR}/${name}.cpp)
-  add_executable(${name} ${test_src})
-  target_compile_definitions(${name} PRIVATE ${CVC5_UNIT_TEST_FLAGS_BLACK})
-  target_link_libraries(${name} PUBLIC main-test GMP)
-  target_link_libraries(${name} PUBLIC GTest::Main)
-  target_link_libraries(${name} PUBLIC GTest::GTest)
+  # Only enable white box unit tests if the compiler supports it and the build
+  # requires it
+  if((NOT ${is_white}) OR ENABLE_WHITEBOX_UNIT_TESTING)
+    set(test_src ${CMAKE_CURRENT_LIST_DIR}/${name}.cpp)
+    add_executable(${name} ${test_src})
+    target_compile_definitions(${name} PRIVATE ${CVC5_UNIT_TEST_FLAGS_BLACK})
+    target_link_libraries(${name} PUBLIC main-test GMP)
+    target_link_libraries(${name} PUBLIC GTest::Main)
+    target_link_libraries(${name} PUBLIC GTest::GTest)
 
-  if(USE_POLY)
-    # Make libpoly headers available for tests
-    target_include_directories(${name} PRIVATE "${Poly_INCLUDE_DIR}")
-  endif()
+    if(USE_POLY)
+      # Make libpoly headers available for tests
+      target_include_directories(${name} PRIVATE "${Poly_INCLUDE_DIR}")
+    endif()
 
-  if(${is_white})
-    target_compile_options(${name} PRIVATE -fno-access-control)
-  endif()
+    if(${is_white})
+      target_compile_options(${name} PRIVATE -fno-access-control)
+    endif()
 
-  # Disable the Wunused-comparison warnings for the unit tests.
-  # We check for `-Wunused-comparison` and then add `-Wno-unused-comparison`
-  check_cxx_compiler_flag("-Wunused-comparison" HAVE_CXX_FLAGWunused_comparison)
-  if(HAVE_CXX_FLAGWunused_comparison)
-    target_compile_options(${name} PRIVATE -Wno-unused-comparison)
-  endif()
-  add_dependencies(build-units ${name})
-  # Generate into bin/test/unit/<output_dir>.
-  set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir})
-  set_target_properties(${name}
-    PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir})
-  # The test target is prefixed with test identifier 'unit/' and the path,
-  # e.g., for '<output_dir>/myunittest.h'
-  #   we create test target 'unit/<output_dir>/myunittest'
-  #   and run it with 'ctest -R "example/<output_dir>/myunittest"'.
-  if("${output_dir}" STREQUAL "")
-    set(test_name unit/${name})
-  else()
-    if("${output_dir}" STREQUAL "api")
-      set(test_name unit/${output_dir}/cpp/${name})
+    # Disable the Wunused-comparison warnings for the unit tests.
+    # We check for `-Wunused-comparison` and then add `-Wno-unused-comparison`
+    check_cxx_compiler_flag("-Wunused-comparison" HAVE_CXX_FLAGWunused_comparison)
+    if(HAVE_CXX_FLAGWunused_comparison)
+      target_compile_options(${name} PRIVATE -Wno-unused-comparison)
+    endif()
+    add_dependencies(build-units ${name})
+    # Generate into bin/test/unit/<output_dir>.
+    set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir})
+    set_target_properties(${name}
+      PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir})
+    # The test target is prefixed with test identifier 'unit/' and the path,
+    # e.g., for '<output_dir>/myunittest.h'
+    #   we create test target 'unit/<output_dir>/myunittest'
+    #   and run it with 'ctest -R "example/<output_dir>/myunittest"'.
+    if("${output_dir}" STREQUAL "")
+      set(test_name unit/${name})
     else()
-      set(test_name unit/${output_dir}/${name})
+      if("${output_dir}" STREQUAL "api")
+        set(test_name unit/${output_dir}/cpp/${name})
+      else()
+        set(test_name unit/${output_dir}/${name})
+      endif()
     endif()
+    add_test(${test_name} ${test_bin_dir}/${name})
+    set_tests_properties(${test_name} PROPERTIES LABELS "unit")
   endif()
-  add_test(${test_name} ${test_bin_dir}/${name})
-  set_tests_properties(${test_name} PROPERTIES LABELS "unit")
 endmacro()
 
 macro(cvc5_add_unit_test_black name output_dir)
@@ -87,14 +91,18 @@ macro(cvc5_add_unit_test_white name output_dir)
   cvc5_add_unit_test(TRUE ${name} ${output_dir})
 endmacro()
 
+# API black box unit tests are always enabled
 add_subdirectory(api)
-add_subdirectory(base)
-add_subdirectory(context)
-add_subdirectory(node)
-add_subdirectory(main)
-add_subdirectory(parser)
-add_subdirectory(printer)
-add_subdirectory(prop)
-add_subdirectory(theory)
-add_subdirectory(preprocessing)
-add_subdirectory(util)
+
+if(ENABLE_UNIT_TESTING)
+  add_subdirectory(base)
+  add_subdirectory(context)
+  add_subdirectory(node)
+  add_subdirectory(main)
+  add_subdirectory(parser)
+  add_subdirectory(printer)
+  add_subdirectory(prop)
+  add_subdirectory(theory)
+  add_subdirectory(preprocessing)
+  add_subdirectory(util)
+endif()
diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index c163e1094..95ee9826f 100644
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -749,7 +749,7 @@ def test_mk_term(solver):
 
     # Test cases that are nary via the API but have arity = 2 internally
     s_bool = solver.getBooleanSort()
-    t_bool = solver.mkConst(s_boo, "t_bool")
+    t_bool = solver.mkConst(s_bool, "t_bool")
     solver.mkTerm(kinds.Implies, [t_bool, t_bool, t_bool])
     solver.mkTerm(kinds.Xor, [t_bool, t_bool, t_bool])
     solver.mkTerm(solver.mkOp(kinds.Xor), [t_bool, t_bool, t_bool])