Refactor and update copyright headers. (#6316)

128 files changed, 1860 insertions, 1823 deletions

diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index 4913a35c1..4ede312f4 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -1,14 +1,18 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Aina Niemetz, Mathias Preiner, Makai Mann
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Aina Niemetz, Mathias Preiner, Yoni Zohar
+#
+# 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.
 ##
-#-----------------------------------------------------------------------------#
+
 # Add target 'check', builds and runs
 # > unit tests
 # > regression tests of levels 0 and 1
diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt
index 7df1342c3..6dadbf759 100644
--- a/test/api/CMakeLists.txt
+++ b/test/api/CMakeLists.txt
@@ -1,13 +1,18 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Aina Niemetz, Andrew V. Jones, Makai Mann
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Aina Niemetz, Andrew V. Jones, Gereon Kremer
+#
+# 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.
 ##
+
 include_directories(.)
 include_directories(${PROJECT_SOURCE_DIR}/src)
 include_directories(${PROJECT_SOURCE_DIR}/src/include)
diff --git a/test/api/boilerplate.cpp b/test/api/boilerplate.cpp
index 73abb3e19..74714a753 100644
--- a/test/api/boilerplate.cpp
+++ b/test/api/boilerplate.cpp
@@ -1,20 +1,21 @@
-/*********************                                                        */
-/*! \file boilerplate.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief A simple start-up/tear-down test for CVC4.
- **
- ** This simple test just makes sure that the public interface is
- ** minimally functional.  It is useful as a template to use for other
- ** system tests.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Andres Noetzli, 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.
+ * ****************************************************************************
+ *
+ * A simple start-up/tear-down test for CVC4.
+ *
+ * This simple test just makes sure that the public interface is
+ * minimally functional.  It is useful as a template to use for other
+ * system tests.
+ */
 
 #include <iostream>
 #include <sstream>
diff --git a/test/api/interactive_shell.py b/test/api/interactive_shell.py
index 0e0ef063c..6660ebe2e 100644
--- a/test/api/interactive_shell.py
+++ b/test/api/interactive_shell.py
@@ -1,29 +1,19 @@
 #!/usr/bin/env python3
-#####################
-## interactive_shell.py
-## Top contributors (to current version):
-##   Andrew V. Jones
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Andrew V. Jones
+#
+# 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.
+# #############################################################################
+#
+# A simple test file to interact with CVC4 with line editing
 ##
 
-#####################
-#! \file interactive_shell.py
-## \verbatim
-## Top contributors (to current version):
-##   Andrew V. Jones
-## This file is part of the CVC4 project.
-## Copyright (c) 2020 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.\endverbatim
-##
-## \brief A simple test file to interact with CVC4 with line editing
-#####################
-
 import sys
 import pexpect
 
diff --git a/test/api/issue4889.cpp b/test/api/issue4889.cpp
index 8fef1cfca..f84d99f42 100644
--- a/test/api/issue4889.cpp
+++ b/test/api/issue4889.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file issue4889.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Test for issue #4889
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * Test for issue #4889
+ */
 
 #include "api/cpp/cvc5.h"
 
diff --git a/test/api/issue5074.cpp b/test/api/issue5074.cpp
index d0000c710..a4f07a581 100644
--- a/test/api/issue5074.cpp
+++ b/test/api/issue5074.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file issue5074.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Test for issue #5074
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli, 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.
+ * ****************************************************************************
+ *
+ * Test for issue #5074
+ */
 
 #include "api/cpp/cvc5.h"
 
diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp
index 96698b4d2..d4aeaf427 100644
--- a/test/api/ouroborous.cpp
+++ b/test/api/ouroborous.cpp
@@ -1,28 +1,29 @@
-/*********************                                                        */
-/*! \file ouroborous.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters, Christopher L. Conway
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief "Ouroborous" test: does CVC4 read its own output?
- **
- ** The "Ouroborous" test, named after the serpent that swallows its
- ** own tail, ensures that CVC4 can parse some input, output it again
- ** (in any of its languages) and then parse it again.  The result of
- ** the first parse must be equal to the result of the second parse;
- ** both strings and expressions are compared for equality.
- **
- ** To add a new test, simply add a call to runTestString() under
- ** runTest(), below.  If you don't specify an input language,
- ** LANG_SMTLIB_V2 is used.  If your example depends on variables,
- ** you'll need to declare them in the "declarations" global, just
- ** below, in SMT-LIBv2 form (but they're good for all languages).
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * "Ouroborous" test: does CVC4 read its own output?
+ *
+ * The "Ouroborous" test, named after the serpent that swallows its
+ * own tail, ensures that CVC4 can parse some input, output it again
+ * (in any of its languages) and then parse it again.  The result of
+ * the first parse must be equal to the result of the second parse;
+ * both strings and expressions are compared for equality.
+ *
+ * To add a new test, simply add a call to runTestString() under
+ * runTest(), below.  If you don't specify an input language,
+ * LANG_SMTLIB_V2 is used.  If your example depends on variables,
+ * you'll need to declare them in the "declarations" global, just
+ * below, in SMT-LIBv2 form (but they're good for all languages).
+ */
 
 #include <cassert>
 #include <iostream>
diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt
index 3aa607c12..af4c8c183 100644
--- a/test/api/python/CMakeLists.txt
+++ b/test/api/python/CMakeLists.txt
@@ -1,15 +1,17 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Makai Mann
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann
+#
+# 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.
 ##
-#-----------------------------------------------------------------------------#
-# Add Python bindings API tests
 
 # Check if the pytest Python module is installed.
 execute_process(
diff --git a/test/api/python/test_datatype_api.py b/test/api/python/test_datatype_api.py
index 72c1af226..81c5478e8 100644
--- a/test/api/python/test_datatype_api.py
+++ b/test/api/python/test_datatype_api.py
@@ -1,13 +1,16 @@
-#####################
-## test_datatype_api.py
-## Top contributors (to current version):
-##   Andres Noetzli, Makai Mann
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Andres Noetzli, Makai Mann
+#
+# 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.
+# #############################################################################
 ##
+
 import pytest
 
 import pycvc4
diff --git a/test/api/python/test_grammar.py b/test/api/python/test_grammar.py
index 9658ea4c6..30f01b59f 100644
--- a/test/api/python/test_grammar.py
+++ b/test/api/python/test_grammar.py
@@ -1,14 +1,16 @@
-#####################
-## test_grammar.py
-## Top contributors (to current version):
-##   Yoni Zohar, Makai Mann, Mudathir Mohamed
-## This file is part of the CVC4 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.
-##
-## Translated from test/unit/api/grammar_black.h
+###############################################################################
+# Top contributors (to current version):
+#   Yoni Zohar, Makai Mann, Mudathir Mohamed
+#
+# 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.
+# #############################################################################
+#
+# Translated from test/unit/api/grammar_black.h
 ##
 
 import pytest
diff --git a/test/api/python/test_sort.py b/test/api/python/test_sort.py
index c05e2b24b..cb8198f98 100644
--- a/test/api/python/test_sort.py
+++ b/test/api/python/test_sort.py
@@ -1,13 +1,16 @@
-#####################
-## test_sort.py
-## Top contributors (to current version):
-##   Makai Mann, Andres Noetzli, Mudathir Mohamed
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann, Andres Noetzli, Mudathir Mohamed
+#
+# 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.
+# #############################################################################
 ##
+
 import pytest
 
 import pycvc4
diff --git a/test/api/python/test_term.py b/test/api/python/test_term.py
index 5a9ac5e0d..e47caaf5c 100644
--- a/test/api/python/test_term.py
+++ b/test/api/python/test_term.py
@@ -1,13 +1,16 @@
-#####################
-## test_term.py
-## Top contributors (to current version):
-##   Makai Mann, Andres Noetzli
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann, Andres Noetzli
+#
+# 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.
+# #############################################################################
 ##
+
 import pytest
 
 import pycvc4
diff --git a/test/api/python/test_to_python_obj.py b/test/api/python/test_to_python_obj.py
index 43ee5cdc9..5d55201de 100644
--- a/test/api/python/test_to_python_obj.py
+++ b/test/api/python/test_to_python_obj.py
@@ -1,13 +1,16 @@
-#####################
-## test_to_python_obj.py
-## Top contributors (to current version):
-##   Makai Mann, Andres Noetzli, Mudathir Mohamed
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann, Andres Noetzli, Mudathir Mohamed
+#
+# 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.
+# #############################################################################
 ##
+
 from fractions import Fraction
 import pytest
 
diff --git a/test/api/reset_assertions.cpp b/test/api/reset_assertions.cpp
index 5e31b0b5e..4c0b06658 100644
--- a/test/api/reset_assertions.cpp
+++ b/test/api/reset_assertions.cpp
@@ -1,21 +1,22 @@
-/*********************                                                        */
-/*! \file reset_assertions.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli, Mudathir Mohamed
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief A simple test for SmtEngine::resetAssertions()
- **
- ** This program indirectly also tests some corner cases w.r.t.
- ** context-dependent datastructures: resetAssertions() pops the contexts to
- ** zero but some context-dependent datastructures are created at leevel 1,
- ** which the datastructure needs to handle properly problematic.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli, Mudathir Mohamed, 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.
+ * ****************************************************************************
+ *
+ * A simple test for SmtEngine::resetAssertions()
+ *
+ * This program indirectly also tests some corner cases w.r.t.
+ * context-dependent datastructures: resetAssertions() pops the contexts to
+ * zero but some context-dependent datastructures are created at leevel 1,
+ * which the datastructure needs to handle properly problematic.
+ */
 
 #include <iostream>
 #include <sstream>
diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp
index 1ce8e9c70..2d37d5c36 100644
--- a/test/api/sep_log_api.cpp
+++ b/test/api/sep_log_api.cpp
@@ -1,23 +1,24 @@
-/*********************                                                        */
-/*! \file sep_log_api.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew V. Jones, Andres Noetzli, Andrew Reynolds
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Two tests to validate the use of the separation logic API.
- **
- ** First test validates that we cannot use the API if not using separation
- ** logic.
- **
- ** Second test validates that the expressions returned from the API are
- ** correct and can be interrogated.
- **
- *****************************************************************************/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew V. Jones, Andres Noetzli, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Two tests to validate the use of the separation logic API.
+ *
+ * First test validates that we cannot use the API if not using separation
+ * logic.
+ *
+ * Second test validates that the expressions returned from the API are
+ * correct and can be interrogated.
+ *
+ ****************************************************************************/
 
 #include <iostream>
 #include <sstream>
diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index a3ae59eda..431bde7d6 100644
--- a/test/api/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file smt2_compliance.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters, Tim King
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief A test of SMT-LIBv2 commands, checks for compliant output
- **
- ** A test of SMT-LIBv2 commands, checks for compliant output.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters, Tim King
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * A test of SMT-LIBv2 commands, checks for compliant output.
+ */
 
 #include <cassert>
 #include <iostream>
diff --git a/test/api/two_solvers.cpp b/test/api/two_solvers.cpp
index b55678b1a..150da1e9e 100644
--- a/test/api/two_solvers.cpp
+++ b/test/api/two_solvers.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file two_solvers.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief A simple test of multiple SmtEngines
- **
- ** A simple test of multiple SmtEngines.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli, Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * A simple test of multiple SmtEngines.
+ */
 
 #include <iostream>
 #include <sstream>
diff --git a/test/java/BitVectors.java b/test/java/BitVectors.java
index 45f4fef0e..3f3d7f5c9 100644
--- a/test/java/BitVectors.java
+++ b/test/java/BitVectors.java
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file BitVectors.java
- ** \verbatim
- ** Top contributors (to current version):
- **   Pat Hawks, Andres Noetzli, Mathias Preiner
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Pat Hawks, Andres Noetzli, 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 import static org.junit.Assert.assertEquals;
 
diff --git a/test/java/BitVectorsAndArrays.java b/test/java/BitVectorsAndArrays.java
index c40b76433..e2ea44d8a 100644
--- a/test/java/BitVectorsAndArrays.java
+++ b/test/java/BitVectorsAndArrays.java
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file BitVectorsAndArrays.java
- ** \verbatim
- ** Top contributors (to current version):
- **   Pat Hawks, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Pat Hawks, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 import static org.junit.Assert.assertEquals;
 
diff --git a/test/java/CMakeLists.txt b/test/java/CMakeLists.txt
index 713bc00bc..3293ca0ab 100644
--- a/test/java/CMakeLists.txt
+++ b/test/java/CMakeLists.txt
@@ -1,13 +1,18 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Mathias Preiner, Andres Noetzli
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Mathias Preiner, Andres Noetzli
+#
+# 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.
 ##
+
 find_package(Java REQUIRED)
 find_package(JUnit 4.0 REQUIRED)
 include(UseJava)
diff --git a/test/java/Combination.java b/test/java/Combination.java
index 995209f4e..21795942b 100644
--- a/test/java/Combination.java
+++ b/test/java/Combination.java
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file Combination.java
- ** \verbatim
- ** Top contributors (to current version):
- **   Pat Hawks, Andres Noetzli, Andrew Reynolds
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Pat Hawks, Andres Noetzli, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 import static org.junit.Assert.assertEquals;
 
diff --git a/test/java/HelloWorld.java b/test/java/HelloWorld.java
index 7c1021245..65cada854 100644
--- a/test/java/HelloWorld.java
+++ b/test/java/HelloWorld.java
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file HelloWorld.java
- ** \verbatim
- ** Top contributors (to current version):
- **   Pat Hawks, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Pat Hawks, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 import static org.junit.Assert.assertEquals;
 
diff --git a/test/java/Issue2846.java b/test/java/Issue2846.java
index 3f7228df7..c7be5e718 100644
--- a/test/java/Issue2846.java
+++ b/test/java/Issue2846.java
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file Issue2846.java
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Test case for issue #2846
- **
- ** This test case tests whether the dependency information for keeping the
- ** ExprManager alive is maintained correctly.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli, Morgan Deters
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Test case for issue #2846
+ *
+ * This test case tests whether the dependency information for keeping the
+ * ExprManager alive is maintained correctly.
+ */
 
 import edu.stanford.CVC4.*;
 import org.junit.Test;
diff --git a/test/java/LinearArith.java b/test/java/LinearArith.java
index c768f4289..8bd0673d9 100644
--- a/test/java/LinearArith.java
+++ b/test/java/LinearArith.java
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file LinearArith.java
- ** \verbatim
- ** Top contributors (to current version):
- **   Pat Hawks, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Pat Hawks, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 import static org.junit.Assert.assertEquals;
 
diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt
index bc652bd10..f3566b6ec 100644
--- a/test/python/CMakeLists.txt
+++ b/test/python/CMakeLists.txt
@@ -1,28 +1,29 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Makai Mann and Yoni Zohar
-## This file is part of the CVC4 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.
+###############################################################################
+# 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.
 ##
-#-----------------------------------------------------------------------------#
-# Add Python bindings API tests
 
 # Check if the pytest Python module is installed.
 check_python_module("pytest")
 
+# Add Python bindings API tests.
 macro(cvc4_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)
-
+# 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
diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index 4ab0427c1..b4a19afa8 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -1,13 +1,16 @@
-#####################
-## test_solver.py
-## Top contributors (to current version):
-##   Yoni Zohar
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Yoni Zohar
+#
+# 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.
+# #############################################################################
 ##
+
 import pytest
 import pycvc4
 import sys
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index dc0a4c980..c40174eda 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1,16 +1,19 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Aina Niemetz, Andrew Reynolds, Mathias Preiner
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Aina Niemetz, Andrew Reynolds, 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.
 ##
-#-----------------------------------------------------------------------------#
-# Regression level 0 tests
 
+# Regression level 0 tests
 set(regress_0_tests
   regress0/arith/ackermann.real.smt2
   regress0/arith/arith-eq.smt2
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index c212a3990..58e43df36 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -1,14 +1,17 @@
 #!/usr/bin/env python3
-#####################
-## run_regression.py
-## Top contributors (to current version):
-##   Andres Noetzli, Yoni Zohar, Mathias Preiner
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Andres Noetzli, Mathias Preiner, Yoni Zohar
+#
+# 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.
+# #############################################################################
 ##
+
 """
 Runs benchmark and checks for correct exit status and output.
 """
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 93ca679f3..e99d92303 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -1,13 +1,18 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Aina Niemetz, Mathias Preiner, Gereon Kremer
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Aina Niemetz, Mathias Preiner, Gereon Kremer
+#
+# 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.
 ##
+
 find_package(GTest REQUIRED)
 include(GoogleTest)
 
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 97564664a..899019b59 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -1,16 +1,19 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Aina Niemetz, Andres Noetzli
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Aina Niemetz, Andres Noetzli
+#
+# 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.
 ##
-#-----------------------------------------------------------------------------#
-# Add unit tests
 
+# Add unit tests.
 cvc4_add_unit_test_black(datatype_api_black api)
 cvc4_add_unit_test_black(grammar_black api)
 cvc4_add_unit_test_black(op_black api)
diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp
index 190816921..7c85f84e0 100644
--- a/test/unit/api/datatype_api_black.cpp
+++ b/test/unit/api/datatype_api_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file datatype_api_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Aina Niemetz, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of the datatype classes of the C++ API.
- **
- ** Black box testing of the datatype classes of the C++ API.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Aina Niemetz, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the datatype classes of the C++ API.
+ */
 
 #include "test_api.h"
 
diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp
index 9c1f750b8..ccab121db 100644
--- a/test/unit/api/grammar_black.cpp
+++ b/test/unit/api/grammar_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file grammar_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of the guards of the C++ API functions.
- **
- ** Black box testing of the guards of the C++ API functions.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Abdalrhman Mohamed
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the guards of the C++ API functions.
+ */
 
 #include "test_api.h"
 
diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp
index 0e6626ec5..0b67c0013 100644
--- a/test/unit/api/op_black.cpp
+++ b/test/unit/api/op_black.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file op_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Makai Mann, Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of the Op class.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Makai Mann, 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the Op class.
+ */
 
 #include "test_api.h"
 
diff --git a/test/unit/api/op_white.cpp b/test/unit/api/op_white.cpp
index 909aafcbb..4953cdd60 100644
--- a/test/unit/api/op_white.cpp
+++ b/test/unit/api/op_white.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file op_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Makai Mann
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of the Op class.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Makai Mann
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of the Op class.
+ */
 
 #include "test_api.h"
 
diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp
index ac4542c59..9bf6b8491 100644
--- a/test/unit/api/result_black.cpp
+++ b/test/unit/api/result_black.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file result_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of the Result class
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the Result class
+ */
 
 #include "test_api.h"
 
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index fef06fa88..c5cdf4f8c 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file solver_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Mudathir Mohamed, Ying Sheng
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of the Solver class of the  C++ API.
- **
- ** Black box testing of the Solver class of the  C++ API.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Mudathir Mohamed, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the Solver class of the  C++ API.
+ */
 
 #include "test_api.h"
 
diff --git a/test/unit/api/solver_white.cpp b/test/unit/api/solver_white.cpp
index 25878f22d..5d7b9eacf 100644
--- a/test/unit/api/solver_white.cpp
+++ b/test/unit/api/solver_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file solver_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Makai Mann, Andrew Reynolds
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of the Solver class of the  C++ API.
- **
- ** Black box testing of the Solver class of the  C++ API.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Makai Mann, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the Solver class of the  C++ API.
+ */
 
 #include "base/configuration.h"
 #include "test_api.h"
diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp
index fa4b1cc9d..8338ffa2c 100644
--- a/test/unit/api/sort_black.cpp
+++ b/test/unit/api/sort_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file sort_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds, Yoni Zohar
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of the guards of the C++ API functions.
- **
- ** Black box testing of the guards of the C++ API functions.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the guards of the C++ API functions.
+ */
 
 #include "test_api.h"
 
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index 117b15394..d894f9720 100644
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file term_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Makai Mann, Andrew Reynolds
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of the Term class.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Makai Mann, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the Term class.
+ */
 
 #include "test_api.h"
 
diff --git a/test/unit/api/term_white.cpp b/test/unit/api/term_white.cpp
index e7b7a9cd6..ace5645dc 100644
--- a/test/unit/api/term_white.cpp
+++ b/test/unit/api/term_white.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file term_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Makai Mann, Aina Niemetz, Andrew Reynolds
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of the Term class.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Makai Mann, Aina Niemetz, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of the Term class.
+ */
 
 #include "test_api.h"
 
diff --git a/test/unit/base/CMakeLists.txt b/test/unit/base/CMakeLists.txt
index 4530c0711..65d352c0b 100644
--- a/test/unit/base/CMakeLists.txt
+++ b/test/unit/base/CMakeLists.txt
@@ -1,14 +1,17 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Aina Niemetz
-## This file is part of the CVC4 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.
+###############################################################################
+# 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.
 ##
-#-----------------------------------------------------------------------------#
-# Add unit tests
 
+# Add unit tests.
 cvc4_add_unit_test_black(map_util_black base)
diff --git a/test/unit/base/map_util_black.cpp b/test/unit/base/map_util_black.cpp
index 3ba866f30..1b5565c1b 100644
--- a/test/unit/base/map_util_black.cpp
+++ b/test/unit/base/map_util_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file map_util_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Tim King
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of map utility functions.
- **
- ** Black box testing of map utility functions.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Tim King
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of map utility functions.
+ */
 
 #include <map>
 #include <set>
diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt
index 9bf07e13c..e5a8caf0f 100644
--- a/test/unit/context/CMakeLists.txt
+++ b/test/unit/context/CMakeLists.txt
@@ -1,16 +1,19 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Aina Niemetz
-## This file is part of the CVC4 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.
+###############################################################################
+# 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.
 ##
-#-----------------------------------------------------------------------------#
-# Add unit tests
 
+# Add unit tests.
 cvc4_add_unit_test_black(cdlist_black context)
 cvc4_add_unit_test_black(cdhashmap_black context)
 cvc4_add_unit_test_white(cdhashmap_white context)
diff --git a/test/unit/context/cdhashmap_black.cpp b/test/unit/context/cdhashmap_black.cpp
index fbeae85b5..c4d744914 100644
--- a/test/unit/context/cdhashmap_black.cpp
+++ b/test/unit/context/cdhashmap_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file cdmap_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::context::CDMap<>.
- **
- ** Black box testing of cvc5::context::CDMap<>.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::context::CDMap<>.
+ */
 
 #include <map>
 
diff --git a/test/unit/context/cdhashmap_white.cpp b/test/unit/context/cdhashmap_white.cpp
index 72e437250..d45c58731 100644
--- a/test/unit/context/cdhashmap_white.cpp
+++ b/test/unit/context/cdhashmap_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file cdmap_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of cvc5::context::CDMap<>.
- **
- ** White box testing of cvc5::context::CDMap<>.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of cvc5::context::CDMap<>.
+ */
 
 #include "base/check.h"
 #include "context/cdhashmap.h"
diff --git a/test/unit/context/cdlist_black.cpp b/test/unit/context/cdlist_black.cpp
index c944b0722..57c25a2b3 100644
--- a/test/unit/context/cdlist_black.cpp
+++ b/test/unit/context/cdlist_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file cdlist_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::context::CDList<>.
- **
- ** Black box testing of cvc5::context::CDList<>.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::context::CDList<>.
+ */
 
 #include <limits.h>
 
diff --git a/test/unit/context/cdo_black.cpp b/test/unit/context/cdo_black.cpp
index c4e9b8dd5..64b6c0700 100644
--- a/test/unit/context/cdo_black.cpp
+++ b/test/unit/context/cdo_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file cdo_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Dejan Jovanovic, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::context::CDO<>.
- **
- ** Black box testing of cvc5::context::CDO<>.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Dejan Jovanovic, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::context::CDO<>.
+ */
 
 #include <iostream>
 #include <vector>
diff --git a/test/unit/context/context_black.cpp b/test/unit/context/context_black.cpp
index ee5140da3..316aa7d46 100644
--- a/test/unit/context/context_black.cpp
+++ b/test/unit/context/context_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file context_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters, Dejan Jovanovic
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::context::Context.
- **
- ** Black box testing of cvc5::context::Context.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters, Dejan Jovanovic
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::context::Context.
+ */
 
 #include <iostream>
 #include <vector>
diff --git a/test/unit/context/context_mm_black.cpp b/test/unit/context/context_mm_black.cpp
index 22b15d70d..d35166193 100644
--- a/test/unit/context/context_mm_black.cpp
+++ b/test/unit/context/context_mm_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file context_mm_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Dejan Jovanovic, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::context::ContextMemoryManager.
- **
- ** Black box testing of cvc5::context::ContextMemoryManager.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Dejan Jovanovic, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::context::ContextMemoryManager.
+ */
 
 #include <cstring>
 #include <iostream>
diff --git a/test/unit/context/context_white.cpp b/test/unit/context/context_white.cpp
index 7bda5d2da..b82fae5dd 100644
--- a/test/unit/context/context_white.cpp
+++ b/test/unit/context/context_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file context_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of cvc5::context::Context.
- **
- ** White box testing of cvc5::context::Context.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of cvc5::context::Context.
+ */
 
 #include "base/check.h"
 #include "context/cdo.h"
diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt
index 6cdf48cb4..36c4cfb48 100644
--- a/test/unit/main/CMakeLists.txt
+++ b/test/unit/main/CMakeLists.txt
@@ -1,14 +1,17 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Aina Niemetz
-## This file is part of the CVC4 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.
+###############################################################################
+# 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.
 ##
-#-----------------------------------------------------------------------------#
-# Add unit tests
 
+# Add unit tests.
 cvc4_add_unit_test_black(interactive_shell_black main)
diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp
index 52f07a2f2..71ad2b1f4 100644
--- a/test/unit/main/interactive_shell_black.cpp
+++ b/test/unit/main/interactive_shell_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file interactive_shell_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Christopher L. Conway, Andrew Reynolds
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::InteractiveShell.
- **
- ** Black box testing of cvc5::InteractiveShell.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Christopher L. Conway, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::InteractiveShell.
+ */
 
 #include <sstream>
 #include <vector>
diff --git a/test/unit/memory.h b/test/unit/memory.h
index 45c65c202..68982077c 100644
--- a/test/unit/memory.h
+++ b/test/unit/memory.h
@@ -1,31 +1,27 @@
-/*********************                                                        */
-/*! \file memory.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Utility class to help testing out-of-memory conditions.
- **
- ** Utility class to help testing out-of-memory conditions.
- **
- ** Use it like this (for example):
- **
- **   cvc5::test::WithLimitedMemory wlm(amount);
- **   TS_ASSERT_THROWS( foo(), bad_alloc );
- **
- ** The WithLimitedMemory destructor will re-establish the previous limit.
- **
- ** This class does not exist in CVC5_MEMORY_LIMITING_DISABLED is defined.
- ** This can be disabled for a variety of reasons.
- ** If this is disabled, there will be a function:
- **   void WarnWithLimitedMemoryDisabledReason()
- ** uses TS_WARN to alert users that these tests are disabled.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Tim King, Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * Utility class to help testing out-of-memory conditions.
+ *
+ * Use it like this (for example):
+ *
+ *   cvc5::test::WithLimitedMemory wlm(amount);
+ *   ASSERT_THROW( foo(), bad_alloc );
+ *
+ * The WithLimitedMemory destructor will re-establish the previous limit.
+ *
+ * This class does not exist in CVC4_MEMORY_LIMITING_DISABLED is defined.
+ * This can be disabled for a variety of reasons.
+ */
 
 #include "test.h"
 
diff --git a/test/unit/node/CMakeLists.txt b/test/unit/node/CMakeLists.txt
index 52e591aeb..5f4c3458c 100644
--- a/test/unit/node/CMakeLists.txt
+++ b/test/unit/node/CMakeLists.txt
@@ -1,16 +1,19 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Aina Niemetz
-## This file is part of the CVC4 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.
+###############################################################################
+# 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.
 ##
-#-----------------------------------------------------------------------------#
-# Add unit tests
 
+# Add unit tests.
 cvc4_add_unit_test_black(attribute_black expr)
 cvc4_add_unit_test_white(attribute_white expr)
 cvc4_add_unit_test_black(kind_black expr)
diff --git a/test/unit/node/attribute_black.cpp b/test/unit/node/attribute_black.cpp
index 0ec1c5e56..ff3aa04d9 100644
--- a/test/unit/node/attribute_black.cpp
+++ b/test/unit/node/attribute_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file attribute_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Tim King, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::Attribute.
- **
- ** Black box testing of cvc5::Attribute.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Tim King, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::Attribute.
+ */
 
 #include <sstream>
 #include <vector>
diff --git a/test/unit/node/attribute_white.cpp b/test/unit/node/attribute_white.cpp
index 59d9500c7..fe74130d1 100644
--- a/test/unit/node/attribute_white.cpp
+++ b/test/unit/node/attribute_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file attribute_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of Node attributes.
- **
- ** White box testing of Node attributes.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of Node attributes.
+ */
 
 #include <string>
 
diff --git a/test/unit/node/kind_black.cpp b/test/unit/node/kind_black.cpp
index defc3aa6f..a0253b728 100644
--- a/test/unit/node/kind_black.cpp
+++ b/test/unit/node/kind_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file kind_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::Kind.
- **
- ** Black box testing of cvc5::Kind.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::Kind.
+ */
 
 #include <iostream>
 #include <sstream>
diff --git a/test/unit/node/kind_map_black.cpp b/test/unit/node/kind_map_black.cpp
index 428da7206..6cc3197d2 100644
--- a/test/unit/node/kind_map_black.cpp
+++ b/test/unit/node/kind_map_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file kind_map_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Gereon Kremer
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::KindMap
- **
- ** Black box testing of cvc5::KindMap.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Gereon Kremer
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::KindMap.
+ */
 
 #include <iostream>
 #include <sstream>
diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp
index 1a739cf1b..6b8c27c17 100644
--- a/test/unit/node/node_algorithm_black.cpp
+++ b/test/unit/node/node_algorithm_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file node_algorithm_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Yoni Zohar, Abdalrhman Mohamed
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of utility functions in node_algorithm.{h,cpp}
- **
- ** Black box testing of node_algorithm.{h,cpp}
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Yoni Zohar, Abdalrhman Mohamed
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of node_algorithm.{h,cpp}
+ */
 
 #include <string>
 #include <vector>
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index b63541d6c..94eb3ae83 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file node_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters, Andrew Reynolds
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::Node.
- **
- ** Black box testing of cvc5::Node.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Morgan Deters
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::Node.
+ */
 
 #include <algorithm>
 #include <sstream>
diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp
index fbf2b9108..fc8b6fb7b 100644
--- a/test/unit/node/node_builder_black.cpp
+++ b/test/unit/node/node_builder_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file node_builder_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Tim King, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::NodeBuilder.
- **
- ** Black box testing of cvc5::NodeBuilder.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andres Noetzli, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::NodeBuilder.
+ */
 
 #include <limits.h>
 
diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp
index a2d25c8d8..7d9d3b556 100644
--- a/test/unit/node/node_manager_black.cpp
+++ b/test/unit/node/node_manager_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file node_manager_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Christopher L. Conway, Dejan Jovanovic
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::NodeManager.
- **
- ** Black box testing of cvc5::NodeManager.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Dejan Jovanovic, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::NodeManager.
+ */
 
 #include <string>
 #include <vector>
diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp
index 986eac870..fe06f85d3 100644
--- a/test/unit/node/node_manager_white.cpp
+++ b/test/unit/node/node_manager_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file node_manager_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of cvc5::NodeManager.
- **
- ** White box testing of cvc5::NodeManager.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andres Noetzli, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of cvc5::NodeManager.
+ */
 
 #include <string>
 
diff --git a/test/unit/node/node_self_iterator_black.cpp b/test/unit/node/node_self_iterator_black.cpp
index fa4889540..66696b71e 100644
--- a/test/unit/node/node_self_iterator_black.cpp
+++ b/test/unit/node/node_self_iterator_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file node_self_iterator_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Tim King, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::expr::NodeSelfIterator
- **
- ** Black box testing of cvc5::expr::NodeSelfIterator
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Tim King
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::expr::NodeSelfIterator.
+ */
 
 #include "expr/node.h"
 #include "expr/node_builder.h"
diff --git a/test/unit/node/node_traversal_black.cpp b/test/unit/node/node_traversal_black.cpp
index 8366b1a63..b8e68c91b 100644
--- a/test/unit/node/node_traversal_black.cpp
+++ b/test/unit/node/node_traversal_black.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file node_traversal_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Alex Ozdemir, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of node traversal iterators.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Alex Ozdemir, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of node traversal iterators.
+ */
 
 #include <algorithm>
 #include <cstddef>
diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp
index 9e3c4bb7d..bf0b8db57 100644
--- a/test/unit/node/node_white.cpp
+++ b/test/unit/node/node_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file node_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of cvc5::Node.
- **
- ** White box testing of cvc5::Node.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of cvc5::Node.
+ */
 
 #include <string>
 
diff --git a/test/unit/node/symbol_table_black.cpp b/test/unit/node/symbol_table_black.cpp
index 7b01b520d..baae33694 100644
--- a/test/unit/node/symbol_table_black.cpp
+++ b/test/unit/node/symbol_table_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file symbol_table_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters, Christopher L. Conway
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::SymbolTable
- **
- ** Black box testing of cvc5::SymbolTable.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters, Christopher L. Conway
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::SymbolTable.
+ */
 
 #include <sstream>
 #include <string>
diff --git a/test/unit/node/type_cardinality_black.cpp b/test/unit/node/type_cardinality_black.cpp
index f0ee99a7d..21e87c5c2 100644
--- a/test/unit/node/type_cardinality_black.cpp
+++ b/test/unit/node/type_cardinality_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file type_cardinality_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Public box testing of Type::getCardinality() for various Types
- **
- ** Public box testing of Type::getCardinality() for various Types.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Public box testing of Type::getCardinality() for various Types.
+ */
 
 #include <string>
 
diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp
index c6f862e03..4fb057fa9 100644
--- a/test/unit/node/type_node_white.cpp
+++ b/test/unit/node/type_node_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file type_node_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of TypeNode
- **
- ** White box testing of TypeNode.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of TypeNode.
+ */
 
 #include <iostream>
 #include <sstream>
diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt
index 216dcdd0f..0044a1d97 100644
--- a/test/unit/parser/CMakeLists.txt
+++ b/test/unit/parser/CMakeLists.txt
@@ -1,15 +1,18 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Aina Niemetz
-## This file is part of the CVC4 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.
+###############################################################################
+# 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.
 ##
-#-----------------------------------------------------------------------------#
-# Add unit tests
 
+# Add unit tests.
 cvc4_add_unit_test_black(parser_black parser)
-cvc4_add_unit_test_black(parser_builder_black parser)
\ No newline at end of file
+cvc4_add_unit_test_black(parser_builder_black parser)
diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp
index 27d008228..1e8e210ca 100644
--- a/test/unit/parser/parser_black.cpp
+++ b/test/unit/parser/parser_black.cpp
@@ -1,19 +1,17 @@
-/*********************                                                        */
-/*! \file parser_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Christopher L. Conway, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::parser::Parser for CVC and SMT-LIBv2
- ** inputs.
- **
- ** Black box testing of cvc5::parser::Parser for CVC and SMT-LIbv2 inputs.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Christopher L. Conway, Morgan Deters
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::parser::Parser for CVC and SMT-LIbv2 inputs.
+ */
 
 #include <sstream>
 
diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp
index 113a5abd5..b8c12eee2 100644
--- a/test/unit/parser/parser_builder_black.cpp
+++ b/test/unit/parser/parser_builder_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file parser_builder_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Christopher L. Conway, Tim King
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::parser::ParserBuilder.
- **
- ** Black box testing of cvc5::parser::ParserBuilder.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Christopher L. Conway, Tim King
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::parser::ParserBuilder.
+ */
 
 #include <stdio.h>
 #include <string.h>
diff --git a/test/unit/preprocessing/CMakeLists.txt b/test/unit/preprocessing/CMakeLists.txt
index 023b8623d..c16cb07fc 100644
--- a/test/unit/preprocessing/CMakeLists.txt
+++ b/test/unit/preprocessing/CMakeLists.txt
@@ -1,15 +1,18 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Aina Niemetz
-## This file is part of the CVC4 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.
+###############################################################################
+# 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.
 ##
-#-----------------------------------------------------------------------------#
-# Add unit tests
 
+# Add unit tests.
 cvc4_add_unit_test_white(pass_bv_gauss_white preprocessing)
-cvc4_add_unit_test_white(pass_foreign_theory_rewrite_white preprocessing)
\ No newline at end of file
+cvc4_add_unit_test_white(pass_foreign_theory_rewrite_white preprocessing)
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index 6f0398439..5905f8404 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file pass_bv_gauss_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Mathias Preiner, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Unit tests for Gaussian Elimination preprocessing pass.
- **
- ** Unit tests for Gaussian Elimination preprocessing pass.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Mathias Preiner, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Unit tests for Gaussian Elimination preprocessing pass.
+ */
 
 #include <iostream>
 #include <vector>
diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
index 662a53777..64b93b3db 100644
--- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
+++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
@@ -1,17 +1,17 @@
-/*********************                                                        */
-/*! \file pass_foreign_theory_rewrite_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Yoni Zohar
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Unit tests for Foreign Theory Rerwrite prepricessing pass
- ** Unit tests for Foreign Theory Rerwrite prepricessing pass
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Yoni Zohar
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Unit tests for Foreign Theory Rerwrite prepricessing pass.
+ */
 
 #include "expr/node_manager.h"
 #include "preprocessing/passes/foreign_theory_rewrite.h"
diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt
index b142d6fab..7cec81221 100644
--- a/test/unit/printer/CMakeLists.txt
+++ b/test/unit/printer/CMakeLists.txt
@@ -1,14 +1,17 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Andres Noetzli, Aina Niemetz
-## This file is part of the CVC4 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.
+###############################################################################
+# 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.
 ##
-#-----------------------------------------------------------------------------#
-# Add unit tests
 
+# Add unit tests.
 cvc4_add_unit_test_black(smt2_printer_black printer)
diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp
index d89930033..a80b27ace 100644
--- a/test/unit/printer/smt2_printer_black.cpp
+++ b/test/unit/printer/smt2_printer_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file smt2_printer_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of the SMT2 printer
- **
- ** Black box testing of the SMT2 printer.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the SMT2 printer.
+ */
 
 #include <iostream>
 
diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt
index 650bbeef0..8e93c14f9 100644
--- a/test/unit/prop/CMakeLists.txt
+++ b/test/unit/prop/CMakeLists.txt
@@ -1,14 +1,17 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Aina Niemetz
-## This file is part of the CVC4 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.
+###############################################################################
+# 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.
 ##
-#-----------------------------------------------------------------------------#
-# Add unit tests
 
+# Add unit tests.
 cvc4_add_unit_test_white(cnf_stream_white prop)
diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp
index 0529f209c..4dfd7a1bb 100644
--- a/test/unit/prop/cnf_stream_white.cpp
+++ b/test/unit/prop/cnf_stream_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file cnf_stream_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Christopher L. Conway, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of cvc5::prop::CnfStream.
- **
- ** White box testing of cvc5::prop::CnfStream.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Christopher L. Conway, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of cvc5::prop::CnfStream.
+ */
 
 #include "base/check.h"
 #include "context/context.h"
diff --git a/test/unit/test.h b/test/unit/test.h
index 383360302..d7035efcd 100644
--- a/test/unit/test.h
+++ b/test/unit/test.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file test.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Common header for API unit test.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Common header for API unit test.
+ */
 
 #ifndef CVC5__TEST__UNIT__TEST_H
 #define CVC5__TEST__UNIT__TEST_H
diff --git a/test/unit/test_api.h b/test/unit/test_api.h
index be0ef46d0..533bdaaa2 100644
--- a/test/unit/test_api.h
+++ b/test/unit/test_api.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file test_api.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Common header for API unit test.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Common header for API unit test.
+ */
 
 #ifndef CVC5__TEST__UNIT__TEST_API_H
 #define CVC5__TEST__UNIT__TEST_API_H
diff --git a/test/unit/test_context.h b/test/unit/test_context.h
index 3ab333806..b034aaa2e 100644
--- a/test/unit/test_context.h
+++ b/test/unit/test_context.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file test_context.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Header for context unit tests.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Header for context unit tests.
+ */
 
 #ifndef CVC5__TEST__UNIT__TEST_CONTEXT_H
 #define CVC5__TEST__UNIT__TEST_CONTEXT_H
diff --git a/test/unit/test_node.h b/test/unit/test_node.h
index ff6ef9b09..4250bb7da 100644
--- a/test/unit/test_node.h
+++ b/test/unit/test_node.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file test_node.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Common header for Node unit tests.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Common header for Node unit tests.
+ */
 
 #ifndef CVC5__TEST__UNIT__TEST_NODE_H
 #define CVC5__TEST__UNIT__TEST_NODE_H
diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index 4307fd1ba..3c19a8c03 100644
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file test_smt.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Common header for unit tests that need an SmtEngine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Haniel Barbosa
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Common header for unit tests that need an SmtEngine.
+ */
 
 #ifndef CVC5__TEST__UNIT__TEST_SMT_H
 #define CVC5__TEST__UNIT__TEST_SMT_H
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index fef2bdd38..75dd8c32c 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -1,13 +1,19 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Aina Niemetz, Michael Chang
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Aina Niemetz, Yoni Zohar, Yancheng Ou
+#
+# 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.
 ##
+
+# Add unit tests.
 cvc4_add_unit_test_black(regexp_operation_black theory)
 cvc4_add_unit_test_black(theory_black theory)
 cvc4_add_unit_test_white(evaluator_white theory)
diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp
index 2afaf3a48..25ffa0572 100644
--- a/test/unit/theory/evaluator_white.cpp
+++ b/test/unit/theory/evaluator_white.cpp
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file evaluator_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 #include <vector>
 
diff --git a/test/unit/theory/logic_info_white.cpp b/test/unit/theory/logic_info_white.cpp
index 5c18b7c98..e51929cad 100644
--- a/test/unit/theory/logic_info_white.cpp
+++ b/test/unit/theory/logic_info_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file logic_info_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Unit testing for cvc5::LogicInfo class
- **
- ** Unit testing for cvc5::LogicInfo class.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Unit testing for cvc5::LogicInfo class.
+ */
 
 #include "base/configuration.h"
 #include "expr/kind.h"
diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp
index 608eeb649..6ba942b6b 100644
--- a/test/unit/theory/regexp_operation_black.cpp
+++ b/test/unit/theory/regexp_operation_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file regexp_operation_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Unit tests for symbolic regular expression operations
- **
- ** Unit tests for symbolic regular expression operations.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Unit tests for symbolic regular expression operations.
+ */
 
 #include <iostream>
 #include <memory>
diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp
index f66a87a83..02472e71e 100644
--- a/test/unit/theory/sequences_rewriter_white.cpp
+++ b/test/unit/theory/sequences_rewriter_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file sequences_rewriter_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andres Noetzli, Andrew Reynolds
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Unit tests for the strings/sequences rewriter
- **
- ** Unit tests for the strings/sequences rewriter.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andres Noetzli, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Unit tests for the strings/sequences rewriter.
+ */
 
 #include <iostream>
 #include <memory>
diff --git a/test/unit/theory/strings_rewriter_white.cpp b/test/unit/theory/strings_rewriter_white.cpp
index 13ee14306..bc6f400c0 100644
--- a/test/unit/theory/strings_rewriter_white.cpp
+++ b/test/unit/theory/strings_rewriter_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file strings_rewriter_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Unit tests for the strings rewriter
- **
- ** Unit tests for the strings rewriter.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Unit tests for the strings rewriter.
+ */
 
 #include <iostream>
 #include <memory>
diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp
index 27ce7158a..4132be8df 100644
--- a/test/unit/theory/theory_arith_white.cpp
+++ b/test/unit/theory/theory_arith_white.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file theory_arith_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Tim King, Dejan Jovanovic
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Whitebox tests for theory Arithmetic.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Tim King, Gereon Kremer
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Whitebox tests for theory Arithmetic.
+ */
 
 #include <list>
 #include <vector>
diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp
index 88a1412a7..88808c018 100644
--- a/test/unit/theory/theory_bags_normal_form_white.cpp
+++ b/test/unit/theory/theory_bags_normal_form_white.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file theory_bags_normal_form_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Mudathir Mohamed
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of bags normal form
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Mudathir Mohamed
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of bags normal form
+ */
 
 #include "expr/dtype.h"
 #include "test_smt.h"
diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp
index 10a606d11..6828e8cdf 100644
--- a/test/unit/theory/theory_bags_rewriter_white.cpp
+++ b/test/unit/theory/theory_bags_rewriter_white.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file theory_bags_rewriter_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Mudathir Mohamed
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of bags rewriter
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Mudathir Mohamed, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of bags rewriter
+ */
 
 #include "expr/dtype.h"
 #include "test_smt.h"
diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp
index 2948c2e9e..4d8270ec6 100644
--- a/test/unit/theory/theory_bags_type_rules_white.cpp
+++ b/test/unit/theory/theory_bags_type_rules_white.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file theory_bags_type_rules_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Mudathir Mohamed
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of bags typing rules
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Mudathir Mohamed
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of bags typing rules
+ */
 
 #include "expr/dtype.h"
 #include "test_smt.h"
diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp
index de3cdaf4d..db4a1e046 100644
--- a/test/unit/theory/theory_black.cpp
+++ b/test/unit/theory/theory_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file theory_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::theory
- **
- ** Black box testing of cvc5::theory
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::theory.
+ */
 
 #include <sstream>
 #include <vector>
diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp
index df1c3755b..ff08a2024 100644
--- a/test/unit/theory/theory_bv_int_blaster_white.cpp
+++ b/test/unit/theory/theory_bv_int_blaster_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file theory_bv_rewriter_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Yoni Zohar
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Unit tests for bit-vector solving via integers
- **
- ** Unit tests for bit-vector solving via integers.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Yoni Zohar
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Unit tests for bit-vector solving via integers.
+ */
 
 #include <iostream>
 #include <memory>
diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp
index fde7a5e2e..386f5b8f8 100644
--- a/test/unit/theory/theory_bv_opt_white.cpp
+++ b/test/unit/theory/theory_bv_opt_white.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file theory_bv_opt_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Yancheng Ou
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White-box testing for optimization module for BitVectors.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Yancheng Ou, Michael Chang
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White-box testing for optimization module for BitVectors.
+ */
 #include <iostream>
 
 #include "smt/optimization_solver.h"
diff --git a/test/unit/theory/theory_bv_rewriter_white.cpp b/test/unit/theory/theory_bv_rewriter_white.cpp
index e0c2dad04..5ea8fa4dd 100644
--- a/test/unit/theory/theory_bv_rewriter_white.cpp
+++ b/test/unit/theory/theory_bv_rewriter_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file theory_bv_rewriter_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Unit tests for the bit-vector rewriter
- **
- ** Unit tests for the bit-vector rewriter.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Unit tests for the bit-vector rewriter.
+ */
 
 #include <iostream>
 #include <memory>
diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp
index bcd91f9b8..bfdcfb604 100644
--- a/test/unit/theory/theory_bv_white.cpp
+++ b/test/unit/theory/theory_bv_white.cpp
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file theory_bv_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Abdalrhman Mohamed, Mathias Preiner
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Abdalrhman Mohamed, 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 #include <vector>
 
diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp
index 57741b98d..dd3426973 100644
--- a/test/unit/theory/theory_engine_white.cpp
+++ b/test/unit/theory/theory_engine_white.cpp
@@ -1,22 +1,22 @@
-/*********************                                                        */
-/*! \file theory_engine_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of cvc5::theory::Theory.
- **
- ** White box testing of cvc5::theory::Theory.  This test creates
- ** "fake" theory interfaces and injects them into TheoryEngine, so we
- ** can test TheoryEngine's behavior without relying on independent
- ** theory behavior.  This is done in TheoryEngineWhite::setUp() by
- ** means of the TheoryEngineWhite::registerTheory() interface.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of cvc5::theory::Theory.
+ *
+ * This test creates "fake" theory interfaces and injects them into
+ * TheoryEngine, so we can test TheoryEngine's behavior without relying on
+ * independent theory behavior.  This is done in TheoryEngineWhite::setUp() by
+ * means of the TheoryEngineWhite::registerTheory() interface.
+ */
 
 #include <memory>
 #include <string>
diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp
index feab15b2b..e8daef819 100644
--- a/test/unit/theory/theory_int_opt_white.cpp
+++ b/test/unit/theory/theory_int_opt_white.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file theory_int_opt_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Michael Chang, Yancheng Ou
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White-box testing for optimization module for Integers.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Michael Chang, Yancheng Ou
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White-box testing for optimization module for Integers.
+ */
 #include <iostream>
 
 #include "smt/optimization_solver.h"
diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
index 19968cbdd..211552590 100644
--- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
+++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file theory_quantifiers_bv_instantiator_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Mathias Preiner, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Unit tests for BvInstantiator.
- **
- ** Unit tests for BvInstantiator.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Mathias Preiner, Andres Noetzli
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Unit tests for BvInstantiator.
+ */
 
 #include <iostream>
 #include <vector>
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
index 92e76d5f5..83d982d8e 100644
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file theory_quantifiers_bv_inverter_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Mathias Preiner, Abdalrhman Mohamed
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Unit tests for BV inverter.
- **
- ** Unit tests for BV inverter.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Mathias Preiner, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Unit tests for BV inverter.
+ */
 
 #include "expr/node.h"
 #include "test_smt.h"
diff --git a/test/unit/theory/theory_sets_type_enumerator_white.cpp b/test/unit/theory/theory_sets_type_enumerator_white.cpp
index f20cf50d2..ecef0773b 100644
--- a/test/unit/theory/theory_sets_type_enumerator_white.cpp
+++ b/test/unit/theory/theory_sets_type_enumerator_white.cpp
@@ -1,21 +1,20 @@
-/*********************                                                        */
-/*! \file theory_sets_type_enumerator_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds, Mudathir Mohamed
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of cvc5::theory::sets::SetsTypeEnumerator
- **
- ** White box testing of cvc5::theory::sets::SetsTypeEnumerator.  (These tests
- ** depends  on the ordering that the SetsTypeEnumerator use, so it's a
- *white-box
- ** test.)
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Mudathir Mohamed
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of cvc5::theory::sets::SetsTypeEnumerator
+ *
+ * These tests depend on the ordering that the SetsTypeEnumerator use, so
+ * it's a white-box test.
+ */
 
 #include "expr/dtype.h"
 #include "test_smt.h"
diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp
index 899a75ae9..d75e5881d 100644
--- a/test/unit/theory/theory_sets_type_rules_white.cpp
+++ b/test/unit/theory/theory_sets_type_rules_white.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file theory_sets_type_rules_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Mudathir Mohamed
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of sets typing rules
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Mudathir Mohamed
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of sets typing rules
+ */
 
 #include "expr/dtype.h"
 #include "test_api.h"
diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp
index 920075674..24cbd166e 100644
--- a/test/unit/theory/theory_strings_skolem_cache_black.cpp
+++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file theory_strings_skolem_cache_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andres Noetzli
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of the skolem cache of the theory of strings.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andres Noetzli, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of the skolem cache of the theory of strings.
+ */
 
 #include <memory>
 
diff --git a/test/unit/theory/theory_strings_word_white.cpp b/test/unit/theory/theory_strings_word_white.cpp
index 1ea73c0cc..9119cf1af 100644
--- a/test/unit/theory/theory_strings_word_white.cpp
+++ b/test/unit/theory/theory_strings_word_white.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file theory_strings_word_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Unit tests for the strings word utilities
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Unit tests for the strings word utilities
+ */
 
 #include <iostream>
 #include <memory>
diff --git a/test/unit/theory/theory_white.cpp b/test/unit/theory/theory_white.cpp
index cb6e5ebfe..5a469ed97 100644
--- a/test/unit/theory/theory_white.cpp
+++ b/test/unit/theory/theory_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file theory_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Tim King, Dejan Jovanovic
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::theory::Theory.
- **
- ** Black box testing of cvc5::theory::Theory.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Dejan Jovanovic
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::theory::Theory.
+ */
 
 #include <memory>
 #include <vector>
diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp
index 6cab15b27..ab77a74ce 100644
--- a/test/unit/theory/type_enumerator_white.cpp
+++ b/test/unit/theory/type_enumerator_white.cpp
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file type_enumerator_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of cvc5::theory::TypeEnumerator
- **
- ** White box testing of cvc5::theory::TypeEnumerator.  (These tests depends
- ** on the ordering that the TypeEnumerators use, so it's a white-box test.)
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Morgan Deters
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of cvc5::theory::TypeEnumerator.
+ *
+ * These tests depend on the ordering that the TypeEnumerators use, so it's a
+ * white-box test.
+ */
 
 #include <unordered_set>
 
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index fc5484a1f..85cc04c94 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -1,16 +1,19 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Aina Niemetz, Yoni Zohar, Gereon Kremer
-## This file is part of the CVC4 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.
+###############################################################################
+# Top contributors (to current version):
+#   Aina Niemetz, Yoni Zohar, Gereon Kremer
+#
+# 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.
 ##
-#-----------------------------------------------------------------------------#
-# Add unit tests
 
+# Add unit tests.
 cvc4_add_unit_test_white(array_store_all_white util)
 cvc4_add_unit_test_white(assert_white util)
 cvc4_add_unit_test_black(binary_heap_black util)
diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp
index b82807835..a33848610 100644
--- a/test/unit/util/array_store_all_white.cpp
+++ b/test/unit/util/array_store_all_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file array_store_all_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::ArrayStoreAll
- **
- ** Black box testing of cvc5::ArrayStoreAll.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::ArrayStoreAll.
+ */
 
 #include "expr/array_store_all.h"
 #include "test_smt.h"
diff --git a/test/unit/util/assert_white.cpp b/test/unit/util/assert_white.cpp
index 245ef8aaa..41a5621c4 100644
--- a/test/unit/util/assert_white.cpp
+++ b/test/unit/util/assert_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file assert_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of cvc5::Configuration.
- **
- ** White box testing of cvc5::Configuration.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of cvc5::Configuration.
+ */
 
 #include <cstring>
 #include <string>
diff --git a/test/unit/util/binary_heap_black.cpp b/test/unit/util/binary_heap_black.cpp
index 76462b687..acbf0871b 100644
--- a/test/unit/util/binary_heap_black.cpp
+++ b/test/unit/util/binary_heap_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file binary_heap_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::BinaryHeap
- **
- ** Black box testing of cvc5::BinaryHeap.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::BinaryHeap.
+ */
 
 #include <iostream>
 #include <sstream>
diff --git a/test/unit/util/bitvector_black.cpp b/test/unit/util/bitvector_black.cpp
index 61dfa8101..2450747cd 100644
--- a/test/unit/util/bitvector_black.cpp
+++ b/test/unit/util/bitvector_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file bitvector_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::BitVector
- **
- ** Black box testing of cvc5::BitVector.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::BitVector.
+ */
 
 #include <sstream>
 
diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp
index 1ec9c923c..4a3afb281 100644
--- a/test/unit/util/boolean_simplification_black.cpp
+++ b/test/unit/util/boolean_simplification_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file boolean_simplification_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters, Tim King
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::BooleanSimplification
- **
- ** Black box testing of cvc5::BooleanSimplification.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters, Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::BooleanSimplification.
+ */
 
 #include <algorithm>
 #include <set>
diff --git a/test/unit/util/cardinality_black.cpp b/test/unit/util/cardinality_black.cpp
index f4b2f3ac4..b19f88ae4 100644
--- a/test/unit/util/cardinality_black.cpp
+++ b/test/unit/util/cardinality_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file cardinality_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Public-box testing of cvc5::Cardinality
- **
- ** Public-box testing of cvc5::Cardinality.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Public-box testing of cvc5::Cardinality.
+ */
 
 #include <sstream>
 #include <string>
diff --git a/test/unit/util/check_white.cpp b/test/unit/util/check_white.cpp
index d517e4364..335c8c3b2 100644
--- a/test/unit/util/check_white.cpp
+++ b/test/unit/util/check_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file check_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Tim King, Mathias Preiner
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of check utilities.
- **
- ** White box testing of check utilities.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Tim King, 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.
+ * ****************************************************************************
+ *
+ * White box testing of check utilities.
+ */
 
 #include <cstring>
 #include <string>
diff --git a/test/unit/util/configuration_black.cpp b/test/unit/util/configuration_black.cpp
index 508aa179b..a651085c6 100644
--- a/test/unit/util/configuration_black.cpp
+++ b/test/unit/util/configuration_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file configuration_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::Configuration.
- **
- ** Black box testing of cvc5::Configuration.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::Configuration.
+ */
 
 #include "base/configuration.h"
 #include "test.h"
diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp
index 37cfe0cfa..3fd817e9d 100644
--- a/test/unit/util/datatype_black.cpp
+++ b/test/unit/util/datatype_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file datatype_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::DType
- **
- ** Black box testing of cvc5::DType.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Morgan Deters
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::DType.
+ */
 
 #include <sstream>
 
diff --git a/test/unit/util/exception_black.cpp b/test/unit/util/exception_black.cpp
index 2884dbfb8..1ebc94b75 100644
--- a/test/unit/util/exception_black.cpp
+++ b/test/unit/util/exception_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file exception_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::Exception.
- **
- ** Black box testing of cvc5::Exception.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::Exception.
+ */
 
 #include <iostream>
 #include <sstream>
diff --git a/test/unit/util/floatingpoint_black.cpp b/test/unit/util/floatingpoint_black.cpp
index 0fe48928f..4bf01151a 100644
--- a/test/unit/util/floatingpoint_black.cpp
+++ b/test/unit/util/floatingpoint_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file floatingpoint_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::FloatingPoint.
- **
- ** Black box testing of cvc5::FloatingPoint.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::FloatingPoint.
+ */
 
 #include "test.h"
 #include "util/floatingpoint.h"
diff --git a/test/unit/util/integer_black.cpp b/test/unit/util/integer_black.cpp
index 1a3e75256..368f12222 100644
--- a/test/unit/util/integer_black.cpp
+++ b/test/unit/util/integer_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file integer_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Tim King
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::Integer.
- **
- ** Black box testing of cvc5::Integer.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Tim King
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::Integer.
+ */
 
 #include <limits>
 #include <sstream>
diff --git a/test/unit/util/integer_white.cpp b/test/unit/util/integer_white.cpp
index 117f82195..a7582ba17 100644
--- a/test/unit/util/integer_white.cpp
+++ b/test/unit/util/integer_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file integer_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Tim King
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of cvc5::Integer.
- **
- ** White box testing of cvc5::Integer.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Tim King
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of cvc5::Integer.
+ */
 
 #include <sstream>
 
diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp
index 09991a6d0..8e9595009 100644
--- a/test/unit/util/output_black.cpp
+++ b/test/unit/util/output_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file output_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters, Tim King
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of CVC4 output classes.
- **
- ** Black box testing of CVC4 output classes.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * Black box testing of CVC4 output classes.
+ */
 
 #include <iostream>
 #include <sstream>
diff --git a/test/unit/util/rational_black.cpp b/test/unit/util/rational_black.cpp
index d3b116d26..d117025a5 100644
--- a/test/unit/util/rational_black.cpp
+++ b/test/unit/util/rational_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file rational_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::Rational.
- **
- ** Black box testing of cvc5::Rational.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::Rational.
+ */
 
 #include <sstream>
 
diff --git a/test/unit/util/rational_white.cpp b/test/unit/util/rational_white.cpp
index c5b52e3c8..20740652e 100644
--- a/test/unit/util/rational_white.cpp
+++ b/test/unit/util/rational_white.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file rational_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Tim King
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief White box testing of cvc5::Rational.
- **
- ** White box testing of cvc5::Rational.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Tim King
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * White box testing of cvc5::Rational.
+ */
 
 #include <sstream>
 
@@ -93,7 +92,7 @@ TEST_F(TestUtilWhiteRational, constructors)
   ASSERT_EQ(dz, qz.getDenominator());
 
   // Not sure how to catch this...
-  // TS_ASSERT_THROWS(Rational div_0(0,0),__gmp_exception );
+  // ASSERT_THROW(Rational div_0(0,0),__gmp_exception );
 }
 
 TEST_F(TestUtilWhiteRational, destructor)
diff --git a/test/unit/util/real_algebraic_number_black.cpp b/test/unit/util/real_algebraic_number_black.cpp
index c130023ca..8969091bd 100644
--- a/test/unit/util/real_algebraic_number_black.cpp
+++ b/test/unit/util/real_algebraic_number_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file real_algebraic_number_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Gereon Kremer
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::RealAlgebraicNumber.
- **
- ** Black box testing of cvc5::RealAlgebraicNumber.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Gereon Kremer
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::RealAlgebraicNumber.
+ */
 
 #include "test.h"
 #include "util/real_algebraic_number.h"
diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp
index c15b0cd47..d2df271d3 100644
--- a/test/unit/util/stats_black.cpp
+++ b/test/unit/util/stats_black.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file stats_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli, Aina Niemetz, Gereon Kremer
- ** This file is part of the CVC4 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.\endverbatim
- **
- ** \brief Black box testing of cvc5::Stat and associated classes
- **
- ** Black box testing of cvc5::Stat and associated classes.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andres Noetzli, Gereon Kremer
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Black box testing of cvc5::Stat and associated classes.
+ */
 
 #include <fcntl.h>