17 files changed, 274 insertions, 281 deletions
diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt
index 225409780..4b3e41ff9 100644
--- a/src/base/CMakeLists.txt
+++ b/src/base/CMakeLists.txt
@@ -1,17 +1,20 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Mathias Preiner, 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.
+###############################################################################
+# Top contributors (to current version):
+#   Mathias Preiner, 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.
+# #############################################################################
+#
+# The build system configuration.
 ##
-#-----------------------------------------------------------------------------#
+
 # Extract info from Git for git_versioninfo.cpp
 # Note: GitInfo.cmake generates git_versioninfo.cpp.
-
 find_package(Git)
 configure_file(GitInfo.cmake.in GitInfo.cmake @ONLY)
 add_custom_target(gen-gitinfo
diff --git a/src/base/GitInfo.cmake.in b/src/base/GitInfo.cmake.in
index 9f8cdfbbe..56a1c5fdb 100644
--- a/src/base/GitInfo.cmake.in
+++ b/src/base/GitInfo.cmake.in
@@ -1,13 +1,16 @@
-#####################
-## GitInfo.cmake.in
-## Top contributors (to current version):
-##   Aina Niemetz, 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, 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.
+# #############################################################################
 ##
+
 set(GIT_BUILD "false")
 set(GIT_IS_DIRTY "false")
 set(GIT_SHA1 "")
diff --git a/src/base/check.cpp b/src/base/check.cpp
index 4bbe8df57..e699202a3 100644
--- a/src/base/check.cpp
+++ b/src/base/check.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file check.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Mathias Preiner, 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 Assertion utility classes, functions and macros.
- **
- ** Implementation of assertion utility classes, functions and macros.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mathias Preiner, 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.
+ * ****************************************************************************
+ *
+ * Assertion utility classes, functions and macros.
+ */
 
 #include "base/check.h"
 
diff --git a/src/base/check.h b/src/base/check.h
index 19329f14f..2905990eb 100644
--- a/src/base/check.h
+++ b/src/base/check.h
@@ -1,33 +1,32 @@
-/*********************                                                        */
-/*! \file check.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Mathias Preiner, Tim King, 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 Assertion utility classes, functions and macros.
- **
- ** The AlwaysAssert utility classes, functions and macros.
- **
- ** The main usage in the file is the AlwaysAssert macros. The AlwaysAssert
- ** macros assert a condition and aborts()'s the process if the condition is
- ** not satisfied. The macro leaves a hanging ostream for the user to specify
- ** additional information about the failure. Example usage:
- **   AlwaysAssert(x >= 0) << "x must be positive.";
- **
- ** Assert is a AlwaysAssert that is only enabled in debug builds.
- **   Assert(pointer != nullptr);
- **
- ** CVC5_FATAL() can be used to indicate unreachable code.
- **
- ** The AlwaysAssert and Assert macros are not safe for use in
- ** signal-handling code. In future, a a signal-handling safe version of
- ** AlwaysAssert may be added.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Tim King, 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.
+ * ****************************************************************************
+ *
+ * Assertion utility classes, functions and macros.
+ *
+ * Assertion macros assert a condition and aborts() the process if the
+ * condition is not satisfied. These macro leave a hanging ostream for the user
+ * to specify additional information about the failure.
+ *
+ * Example usage:
+ *   AlwaysAssert(x >= 0) << "x must be positive.";
+ *
+ * Assert is an AlwaysAssert that is only enabled in debug builds.
+ *   Assert(pointer != nullptr);
+ *
+ * CVC5_FATAL() can be used to indicate unreachable code.
+ *
+ * Note: The AlwaysAssert and Assert macros are not safe for use in
+ *       signal-handling code.
+ */
 
 #include "cvc4_private_library.h"
 
diff --git a/src/base/collect_tags.py b/src/base/collect_tags.py
index 2d4952a47..43e183b99 100644
--- a/src/base/collect_tags.py
+++ b/src/base/collect_tags.py
@@ -1,13 +1,15 @@
 #!/usr/bin/env python3
-#####################
-## collect_tags.py
-## Top contributors (to current version):
-##   Gereon Kremer, 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):
+#   Gereon Kremer, 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.
+# #############################################################################
 ##
 
 import argparse
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 74bcdc57f..dc0cc2ffb 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -1,20 +1,18 @@
-/*********************                                                        */
-/*! \file configuration.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Aina Niemetz, 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 Implementation of Configuration class, which provides compile-time
- ** configuration information about the CVC4 library
- **
- ** Implementation of Configuration class, which provides compile-time
- ** configuration information about the CVC4 library.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * Implementation of Configuration class, which provides compile-time
+ * configuration information about the CVC4 library.
+ */
 #include "base/configuration.h"
 
 #include <stdlib.h>
diff --git a/src/base/configuration.h b/src/base/configuration.h
index 3d30682fd..66f3b8566 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -1,20 +1,18 @@
-/*********************                                                        */
-/*! \file configuration.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Francois Bobot, 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 Interface to a public class that provides compile-time information
- ** about the CVC4 library.
- **
- ** Interface to a public class that provides compile-time information
- ** about the CVC4 library.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Gereon Kremer, 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.
+ * ****************************************************************************
+ *
+ * Interface to a public class that provides compile-time information
+ * about the CVC4 library.
+ */
 
 #include "cvc4_public.h"
 
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index ce6397682..8b43b5cab 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -1,17 +1,17 @@
-/*********************                                                        */
-/*! \file configuration_private.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Christopher L. Conway, 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 Provides compile-time configuration information about the
- ** CVC4 library.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Christopher L. Conway, 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.
+ * ****************************************************************************
+ *
+ * Provide compile-time configuration information about the cvc5 library.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index c6fb03834..b337f819a 100644
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file exception.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Morgan Deters, 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 CVC4's exception base class and some associated utilities
- **
- ** CVC4's exception base class and some associated utilities.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Tim King, Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * cvc5's exception base class and some associated utilities.
+ */
 
 #include "base/exception.h"
 
diff --git a/src/base/exception.h b/src/base/exception.h
index 579a8cdad..b7bc00d71 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file exception.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, 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 CVC4's exception base class and some associated utilities
- **
- ** CVC4's exception base class and some associated utilities.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * cvc5's exception base class and some associated utilities.
+ */
 
 #include "cvc4_public.h"
 
diff --git a/src/base/git_versioninfo.cpp.in b/src/base/git_versioninfo.cpp.in
index 1f8c82ee8..3db99fe15 100644
--- a/src/base/git_versioninfo.cpp.in
+++ b/src/base/git_versioninfo.cpp.in
@@ -1,19 +1,17 @@
-/*********************                                                        */
-/*! \file git_versioninfo.cpp.in
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, 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
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Compile version info from git.
+ */
 
 #include "base/configuration.h"
 const bool ::cvc5::Configuration::IS_GIT_BUILD = @GIT_BUILD@;
diff --git a/src/base/listener.cpp b/src/base/listener.cpp
index 6faf7635b..2c9fc9b22 100644
--- a/src/base/listener.cpp
+++ b/src/base/listener.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file listener.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   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 Output utility classes and functions
- **
- ** Output utility classes and functions.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   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.
+ * ****************************************************************************
+ *
+ * Output utility classes and functions.
+ */
 
 #include "base/listener.h"
 
diff --git a/src/base/listener.h b/src/base/listener.h
index dc5078862..ee42d4359 100644
--- a/src/base/listener.h
+++ b/src/base/listener.h
@@ -1,19 +1,19 @@
-/*********************                                                        */
-/*! \file listener.h
- ** \verbatim
- ** Top contributors (to current version):
- **   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 Utility classes for listeners and collections of listeners.
- **
- ** Utilities for the development of a Listener interface class. This class
- ** provides a single notification that must be overwritten.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   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.
+ * ****************************************************************************
+ *
+ * Utilities for the development of a Listener interface class.
+ *
+ * This class provides a single notification that must be overwritten.
+ */
 
 #include "cvc4_public.h"
 
diff --git a/src/base/map_util.h b/src/base/map_util.h
index 93dac21f2..4c46052a1 100644
--- a/src/base/map_util.h
+++ b/src/base/map_util.h
@@ -1,37 +1,37 @@
-/*********************                                                        */
-/*! \file map_util.h
- ** \verbatim
- ** Top contributors (to current version):
- **   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 Utility functions for dealing with maps in a mostly uniform fashion.
- **
- ** Utility functions for dealing with maps and related classed in a mostly
- ** uniform fashion. These are stylistically encouraged (but not required) in
- ** new code. Supports:
- ** - std::map
- ** - std::unordered_map
- ** - cvc5::context::CDHashmap
- ** - cvc5::context::CDInsertHashmap
- ** The ContainsKey function is also compatible with std::[unordered_]set.
- **
- ** Currently implemented classes of functions:
- ** - ContainsKey
- **   Returns true if a map contains a key. (Also Supports std::set and
- **   std::unordered_set.)
- ** - FindOr*
- **   Finds an data element mapped to by the map. Variants include FindOrNull
- **   and FindOrDie.
- **
- ** Potential future classes of functions:
- ** - InsertOrUpdate
- ** - InsertIfNotPresent
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   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.
+ * ****************************************************************************
+ * Utility functions for dealing with maps and related classes in a mostly
+ * uniform fashion.
+ *
+ * These are stylistically encouraged (but not required) in new code.
+ * Supports:
+ * - std::map
+ * - std::unordered_map
+ * - cvc5::context::CDHashmap
+ * - cvc5::context::CDInsertHashmap
+ * The ContainsKey function is also compatible with std::[unordered_]set.
+ *
+ * Currently implemented classes of functions:
+ * - ContainsKey
+ *   Returns true if a map contains a key. (Also Supports std::set and
+ *   std::unordered_set.)
+ * - FindOr*
+ *   Finds an data element mapped to by the map. Variants include FindOrNull
+ *   and FindOrDie.
+ *
+ * Potential future classes of functions:
+ * - InsertOrUpdate
+ * - InsertIfNotPresent
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/base/modal_exception.h b/src/base/modal_exception.h
index d6b941dd3..bf019f707 100644
--- a/src/base/modal_exception.h
+++ b/src/base/modal_exception.h
@@ -1,21 +1,19 @@
-/*********************                                                        */
-/*! \file modal_exception.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, 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 An exception that is thrown when an interactive-only
- ** feature while CVC4 is being used in a non-interactive setting
- **
- ** An exception that is thrown when an interactive-only feature while
- ** CVC4 is being used in a non-interactive setting (for example, the
- ** "(get-assertions)" command in an SMT-LIBv2 script).
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * An exception that is thrown when an interactive-only feature while
+ * CVC4 is being used in a non-interactive setting (for example, the
+ * "(get-assertions)" command in an SMT-LIBv2 script).
+ */
 
 #include "cvc4_public.h"
 
diff --git a/src/base/output.cpp b/src/base/output.cpp
index f24e0f7fb..9e0e452f2 100644
--- a/src/base/output.cpp
+++ b/src/base/output.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file output.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   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 Output utility classes and functions
- **
- ** Output utility classes and functions.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mathias Preiner, 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.
+ * ****************************************************************************
+ *
+ * Output utility classes and functions.
+ */
 
 #include "base/output.h"
 
diff --git a/src/base/output.h b/src/base/output.h
index acad7e40b..4a7be543e 100644
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file output.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Andres Noetzli, 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 Output utility classes and functions
- **
- ** Output utility classes and functions.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * Output utility classes and functions.
+ */
 
 #include "cvc4_private_library.h"