16 files changed, 241 insertions, 226 deletions
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>