Refactor and update copyright headers. (#6316)

19 files changed, 267 insertions, 282 deletions

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>