25 files changed, 88 insertions, 63 deletions
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index d3ff709ca..5f96d2b9b 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -41,8 +41,3 @@ add_subdirectory(api EXCLUDE_FROM_ALL)
 if(ENABLE_UNIT_TESTING)
   add_subdirectory(unit EXCLUDE_FROM_ALL)
 endif()
-
-# add Python bindings tests if building with Python bindings
-if (BUILD_BINDINGS_PYTHON)
-  add_subdirectory(python)
-endif()
diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt
deleted file mode 100644
index 5b681ca36..000000000
--- a/test/python/CMakeLists.txt
+++ /dev/null
@@ -1,37 +0,0 @@
-###############################################################################
-# Top contributors (to current version):
-#   Yoni Zohar, Aina Niemetz, Mathias Preiner
-#
-# This file is part of the cvc5 project.
-#
-# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
-# in the top-level source directory and their institutional affiliations.
-# All rights reserved.  See the file COPYING in the top-level source
-# directory for licensing information.
-# #############################################################################
-#
-# The build system configuration.
-##
-
-# Check if the pytest Python module is installed.
-check_python_module("pytest")
-
-# Add Python bindings API tests.
-macro(cvc5_add_python_api_test name filename)
-# We create test target 'python/unit/api/myapitest' and run it with
-# 'ctest -R "python/unit/api/myapitest"'.
-add_test (NAME python/unit/api/${name}
-  COMMAND ${PYTHON_EXECUTABLE} -m pytest ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
-  # directory for importing the python bindings
-  WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python)
-endmacro()
-
-# add specific test files
-cvc5_add_python_api_test(pytest_solver unit/api/test_solver.py)
-cvc5_add_python_api_test(pytest_sort unit/api/test_sort.py)
-cvc5_add_python_api_test(pytest_term unit/api/test_term.py)
-cvc5_add_python_api_test(pytest_datatype_api unit/api/test_datatype_api.py)
-cvc5_add_python_api_test(pytest_grammar unit/api/test_grammar.py)
-cvc5_add_python_api_test(pytest_to_python_obj unit/api/test_to_python_obj.py)
-cvc5_add_python_api_test(pytest_op unit/api/test_op.py)
-cvc5_add_python_api_test(pytest_result unit/api/test_result.py)
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 11c2e8514..9be9dcefa 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -70,7 +70,11 @@ macro(cvc5_add_unit_test is_white name output_dir)
   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")
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index ae6db51ef..0701c3ca6 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -13,17 +13,10 @@
 # The build system configuration.
 ##
 
-# Add unit tests.
-cvc5_add_unit_test_black(datatype_api_black api)
-cvc5_add_unit_test_black(grammar_black api)
-cvc5_add_unit_test_black(op_black api)
-cvc5_add_unit_test_white(op_white api)
-cvc5_add_unit_test_black(result_black api)
-cvc5_add_unit_test_black(solver_black api)
-cvc5_add_unit_test_white(solver_white api)
-cvc5_add_unit_test_black(sort_black api)
-cvc5_add_unit_test_black(term_black api)
-cvc5_add_unit_test_white(term_white api)
+add_subdirectory(cpp)
+if (BUILD_BINDINGS_PYTHON)
+  add_subdirectory(python)
+endif()
 if (BUILD_BINDINGS_JAVA)
   add_subdirectory(java)
 endif()
diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt
new file mode 100644
index 000000000..e99732ca4
--- /dev/null
+++ b/test/unit/api/cpp/CMakeLists.txt
@@ -0,0 +1,24 @@
+###############################################################################
+# Top contributors (to current version):
+#   Aina Niemetz
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# The build system configuration.
+##
+cvc5_add_unit_test_black(datatype_api_black api)
+cvc5_add_unit_test_black(grammar_black api)
+cvc5_add_unit_test_black(op_black api)
+cvc5_add_unit_test_white(op_white api)
+cvc5_add_unit_test_black(result_black api)
+cvc5_add_unit_test_black(solver_black api)
+cvc5_add_unit_test_white(solver_white api)
+cvc5_add_unit_test_black(sort_black api)
+cvc5_add_unit_test_black(term_black api)
+cvc5_add_unit_test_white(term_white api)
diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp
index 745abc17c..745abc17c 100644
--- a/test/unit/api/datatype_api_black.cpp
+++ b/test/unit/api/cpp/datatype_api_black.cpp
diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/cpp/grammar_black.cpp
index 7b7556539..7b7556539 100644
--- a/test/unit/api/grammar_black.cpp
+++ b/test/unit/api/cpp/grammar_black.cpp
diff --git a/test/unit/api/op_black.cpp b/test/unit/api/cpp/op_black.cpp
index fd45b1c22..fd45b1c22 100644
--- a/test/unit/api/op_black.cpp
+++ b/test/unit/api/cpp/op_black.cpp
diff --git a/test/unit/api/op_white.cpp b/test/unit/api/cpp/op_white.cpp
index 39952739b..39952739b 100644
--- a/test/unit/api/op_white.cpp
+++ b/test/unit/api/cpp/op_white.cpp
diff --git a/test/unit/api/result_black.cpp b/test/unit/api/cpp/result_black.cpp
index 9bf6b8491..9bf6b8491 100644
--- a/test/unit/api/result_black.cpp
+++ b/test/unit/api/cpp/result_black.cpp
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 79a4aa63e..37aed63be 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -15,8 +15,8 @@
 
 #include <algorithm>
 
-#include "test_api.h"
 #include "base/output.h"
+#include "test_api.h"
 
 namespace cvc5 {
 
@@ -341,9 +341,12 @@ TEST_F(TestApiBlackSolver, mkBitVector)
 
   ASSERT_EQ(d_solver.mkBitVector(8, "0101", 2),
             d_solver.mkBitVector(8, "00000101", 2));
-  ASSERT_EQ(d_solver.mkBitVector(4, "-1", 2), d_solver.mkBitVector(4, "1111", 2));
-  ASSERT_EQ(d_solver.mkBitVector(4, "-1", 16), d_solver.mkBitVector(4, "1111", 2));
-  ASSERT_EQ(d_solver.mkBitVector(4, "-1", 10), d_solver.mkBitVector(4, "1111", 2));
+  ASSERT_EQ(d_solver.mkBitVector(4, "-1", 2),
+            d_solver.mkBitVector(4, "1111", 2));
+  ASSERT_EQ(d_solver.mkBitVector(4, "-1", 16),
+            d_solver.mkBitVector(4, "1111", 2));
+  ASSERT_EQ(d_solver.mkBitVector(4, "-1", 10),
+            d_solver.mkBitVector(4, "1111", 2));
   ASSERT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101");
   ASSERT_EQ(d_solver.mkBitVector(8, "F", 16).toString(), "#b00001111");
   ASSERT_EQ(d_solver.mkBitVector(8, "-1", 10),
@@ -1351,7 +1354,8 @@ TEST_F(TestApiBlackSolver, getOptionInfo)
     api::OptionInfo info = d_solver.getOptionInfo("verbosity");
     EXPECT_EQ("verbosity", info.name);
     EXPECT_EQ(std::vector<std::string>{}, info.aliases);
-    EXPECT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(info.valueInfo));
+    EXPECT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(
+        info.valueInfo));
     auto numInfo = std::get<OptionInfo::NumberInfo<int64_t>>(info.valueInfo);
     EXPECT_EQ(0, numInfo.defaultValue);
     EXPECT_EQ(0, numInfo.currentValue);
@@ -1362,7 +1366,8 @@ TEST_F(TestApiBlackSolver, getOptionInfo)
     auto info = d_solver.getOptionInfo("random-freq");
     ASSERT_EQ(info.name, "random-freq");
     ASSERT_EQ(info.aliases, std::vector<std::string>{"random-frequency"});
-    ASSERT_TRUE(std::holds_alternative<api::OptionInfo::NumberInfo<double>>(info.valueInfo));
+    ASSERT_TRUE(std::holds_alternative<api::OptionInfo::NumberInfo<double>>(
+        info.valueInfo));
     auto ni = std::get<api::OptionInfo::NumberInfo<double>>(info.valueInfo);
     ASSERT_EQ(ni.currentValue, 0.0);
     ASSERT_EQ(ni.defaultValue, 0.0);
@@ -2540,7 +2545,6 @@ TEST_F(TestApiBlackSolver, Output)
   ASSERT_NE(cvc5::null_os.rdbuf(), d_solver.getOutput("inst").rdbuf());
 }
 
-
 TEST_F(TestApiBlackSolver, issue7000)
 {
   Sort s1 = d_solver.getIntegerSort();
diff --git a/test/unit/api/solver_white.cpp b/test/unit/api/cpp/solver_white.cpp
index 5d7b9eacf..5d7b9eacf 100644
--- a/test/unit/api/solver_white.cpp
+++ b/test/unit/api/cpp/solver_white.cpp
diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp
index d0c755cf7..d0c755cf7 100644
--- a/test/unit/api/sort_black.cpp
+++ b/test/unit/api/cpp/sort_black.cpp
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/cpp/term_black.cpp
index 9e52174b4..f4180aa34 100644
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/cpp/term_black.cpp
@@ -807,10 +807,12 @@ TEST_F(TestApiBlackTerm, getReal)
   ASSERT_EQ((std::pair<int64_t, uint64_t>(127, 10)), real5.getReal64Value());
   ASSERT_EQ("127/10", real5.getRealValue());
 
-  ASSERT_EQ((std::pair<int64_t, uint64_t>(1, 4294967297)), real6.getReal64Value());
+  ASSERT_EQ((std::pair<int64_t, uint64_t>(1, 4294967297)),
+            real6.getReal64Value());
   ASSERT_EQ("1/4294967297", real6.getRealValue());
 
-  ASSERT_EQ((std::pair<int64_t, uint64_t>(4294967297, 1)), real7.getReal64Value());
+  ASSERT_EQ((std::pair<int64_t, uint64_t>(4294967297, 1)),
+            real7.getReal64Value());
   ASSERT_EQ("4294967297/1", real7.getRealValue());
 
   ASSERT_EQ("1/18446744073709551617", real8.getRealValue());
diff --git a/test/unit/api/term_white.cpp b/test/unit/api/cpp/term_white.cpp
index ace5645dc..ace5645dc 100644
--- a/test/unit/api/term_white.cpp
+++ b/test/unit/api/cpp/term_white.cpp
diff --git a/test/unit/api/python/CMakeLists.txt b/test/unit/api/python/CMakeLists.txt
new file mode 100644
index 000000000..cbf9629ce
--- /dev/null
+++ b/test/unit/api/python/CMakeLists.txt
@@ -0,0 +1,40 @@
+###############################################################################
+# Top contributors (to current version):
+#   Yoni Zohar, Aina Niemetz, Mathias Preiner
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# The build system configuration.
+##
+
+# Check if the pytest Python module is installed.
+check_python_module("pytest")
+
+# Add Python bindings API tests.
+macro(cvc5_add_python_api_unit_test name filename)
+# We create test target 'python/unit/api/myapitest' and run it with
+# 'ctest -R "python/unit/api/myapitest"'.
+  set(test_name unit/api/python/${name})
+  add_test (NAME ${test_name}
+    COMMAND ${PYTHON_EXECUTABLE}
+            -m pytest ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
+    # directory for importing the python bindings
+    WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python)
+    set_tests_properties(${test_name} PROPERTIES LABELS "unit")
+endmacro()
+
+# add specific test files
+cvc5_add_python_api_unit_test(pytest_solver test_solver.py)
+cvc5_add_python_api_unit_test(pytest_sort test_sort.py)
+cvc5_add_python_api_unit_test(pytest_term test_term.py)
+cvc5_add_python_api_unit_test(pytest_datatype_api test_datatype_api.py)
+cvc5_add_python_api_unit_test(pytest_grammar test_grammar.py)
+cvc5_add_python_api_unit_test(pytest_to_python_obj test_to_python_obj.py)
+cvc5_add_python_api_unit_test(pytest_op test_op.py)
+cvc5_add_python_api_unit_test(pytest_result test_result.py)
diff --git a/test/python/unit/api/__init__.py b/test/unit/api/python/__init__.py
index e69de29bb..e69de29bb 100644
--- a/test/python/unit/api/__init__.py
+++ b/test/unit/api/python/__init__.py
diff --git a/test/python/unit/api/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py
index d8a4c26f7..d8a4c26f7 100644
--- a/test/python/unit/api/test_datatype_api.py
+++ b/test/unit/api/python/test_datatype_api.py
diff --git a/test/python/unit/api/test_grammar.py b/test/unit/api/python/test_grammar.py
index db567a6ba..db567a6ba 100644
--- a/test/python/unit/api/test_grammar.py
+++ b/test/unit/api/python/test_grammar.py
diff --git a/test/python/unit/api/test_op.py b/test/unit/api/python/test_op.py
index 5126a481d..5126a481d 100644
--- a/test/python/unit/api/test_op.py
+++ b/test/unit/api/python/test_op.py
diff --git a/test/python/unit/api/test_result.py b/test/unit/api/python/test_result.py
index bd97646f9..bd97646f9 100644
--- a/test/python/unit/api/test_result.py
+++ b/test/unit/api/python/test_result.py
diff --git a/test/python/unit/api/test_solver.py b/test/unit/api/python/test_solver.py
index 71ab17465..71ab17465 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/unit/api/python/test_solver.py
diff --git a/test/python/unit/api/test_sort.py b/test/unit/api/python/test_sort.py
index 98cf76d76..98cf76d76 100644
--- a/test/python/unit/api/test_sort.py
+++ b/test/unit/api/python/test_sort.py
diff --git a/test/python/unit/api/test_term.py b/test/unit/api/python/test_term.py
index 34a79d597..34a79d597 100644
--- a/test/python/unit/api/test_term.py
+++ b/test/unit/api/python/test_term.py
diff --git a/test/python/unit/api/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py
index bb30fae8f..bb30fae8f 100644
--- a/test/python/unit/api/test_to_python_obj.py
+++ b/test/unit/api/python/test_to_python_obj.py