Refactor and update copyright headers. (#6316)

26 files changed, 399 insertions, 393 deletions

diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 574432085..77c4d5a09 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -1,15 +1,19 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Mathias Preiner, 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.
+###############################################################################
+# Top contributors (to current version):
+#   Mathias Preiner, 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.
+# #############################################################################
+#
+# The build system configuration.
 ##
-# Check if the toml Python module is installed.
 
+# Check if the toml Python module is installed.
 check_python_module("toml")
 
 libcvc4_add_sources(
diff --git a/src/options/base_handlers.h b/src/options/base_handlers.h
index 027412f5a..37389180f 100644
--- a/src/options/base_handlers.h
+++ b/src/options/base_handlers.h
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file base_handlers.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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/options/decision_weight.h b/src/options/decision_weight.h
index ffc2a3626..c4e8ef9b6 100644
--- a/src/options/decision_weight.h
+++ b/src/options/decision_weight.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file decision_weight.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Mathias Preiner, Kshitij Bansal
- ** 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 Rewriter attributes
- **
- ** Rewriter attributes.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mathias Preiner, Kshitij Bansal
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Rewriter attributes.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/options/didyoumean.cpp b/src/options/didyoumean.cpp
index 8f539cdd3..49e3a2270 100644
--- a/src/options/didyoumean.cpp
+++ b/src/options/didyoumean.cpp
@@ -1,21 +1,22 @@
-/*********************                                                        */
-/*! \file didyoumean.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Kshitij Bansal, Tim King, Clark Barrett
- ** 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 did-you-mean style suggestions
- **
- ** ``What do you mean? I don't understand.'' An attempt to be more
- ** helpful than that. Similar to one in git.
- **
- ** There are no dependencies on CVC4 (except namespace).
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Kshitij Bansal, Tim King, Clark Barrett
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Did-you-mean style suggestions.
+ *
+ * ``What do you mean? I don't understand.'' An attempt to be more
+ * helpful than that. Similar to one in git.
+ *
+ * There are no dependencies on CVC4 (except namespace).
+ */
 
 #include "options/didyoumean.h"
 
diff --git a/src/options/didyoumean.h b/src/options/didyoumean.h
index e0da600b8..ad3c08d24 100644
--- a/src/options/didyoumean.h
+++ b/src/options/didyoumean.h
@@ -1,21 +1,22 @@
-/*********************                                                        */
-/*! \file didyoumean.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Kshitij Bansal, 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 did-you-mean style suggestions.
- **
- ** ``What do you mean? I don't understand.'' An attempt to be more
- ** helpful than that. Similar to one in git.
- **
- ** There are no dependencies on CVC4 (except namespace).
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Kshitij Bansal, 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.
+ * ****************************************************************************
+ *
+ * Did-you-mean style suggestions.
+ *
+ * ``What do you mean? I don't understand.'' An attempt to be more
+ * helpful than that. Similar to one in git.
+ *
+ * There are no dependencies on CVC4 (except namespace).
+ */
 
 #pragma once
 
diff --git a/src/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp
index f4791db95..57d932b61 100644
--- a/src/options/didyoumean_test.cpp
+++ b/src/options/didyoumean_test.cpp
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file didyoumean_test.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Kshitij Bansal, Tim King, 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):
+ *   Kshitij Bansal, 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 // This is not built as a part of CVC4 and is not built by Makefile.am.
 // Compile: g++ didyoumean_test.cpp didyoumean.cpp
diff --git a/src/options/language.cpp b/src/options/language.cpp
index 8fb1ad53a..8261271fb 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file language.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, 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.\endverbatim
- **
- ** \brief Definition of input and output languages
- **
- ** Definition of input and output languages.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * Definition of input and output languages.
+ */
 
 #include "options/language.h"
 
diff --git a/src/options/language.h b/src/options/language.h
index 69a349c61..07dc5da7b 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file language.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Francois Bobot
- ** 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 Definition of input and output languages
- **
- ** Definition of input and output languages.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * Definition of input and output languages.
+ */
 
 #include "cvc4_public.h"
 
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 9fbcf7158..b93186767 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -1,14 +1,17 @@
 #!/usr/bin/env python
-#####################
-## mkoptions.py
-## Top contributors (to current version):
-##   Mathias Preiner, Everett Maus
-## 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, Everett Maus
+#
+# 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.
+# #############################################################################
 ##
+
 """
     Generate option handling code and documentation in one pass. The generated
     files are only written to the destination file if the contents of the file
diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp
index c05017c70..3b928dba0 100644
--- a/src/options/module_template.cpp
+++ b/src/options/module_template.cpp
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file module_template.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   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 Option template for option modules.
- **
- ** For each <module>_options.toml configuration file, mkoptions.py
- ** expands this template and generates a <module>_options.cpp file.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mathias Preiner, 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.
+ * ****************************************************************************
+ *
+ * Option template for option modules.
+ *
+ * For each <module>_options.toml configuration file, mkoptions.py
+ * expands this template and generates a <module>_options.cpp file.
+ */
 
 #include "options/options_holder.h"
 #include "base/check.h"
diff --git a/src/options/module_template.h b/src/options/module_template.h
index 2e5e402fc..279831fcc 100644
--- a/src/options/module_template.h
+++ b/src/options/module_template.h
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file module_template.h
- ** \verbatim
- ** Top contributors (to current version):
- **   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 Contains code for handling command-line options.
- **
- ** For each <module>_options.toml configuration file, mkoptions.py
- ** expands this template and generates a <module>_options.h file.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mathias Preiner, 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.
+ * ****************************************************************************
+ *
+ * Contains code for handling command-line options.
+ *
+ * For each <module>_options.toml configuration file, mkoptions.py
+ * expands this template and generates a <module>_options.h file.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp
index 850fdce80..fa36738d9 100644
--- a/src/options/open_ostream.cpp
+++ b/src/options/open_ostream.cpp
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file open_ostream.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 #include "options/open_ostream.h"
 
diff --git a/src/options/open_ostream.h b/src/options/open_ostream.h
index 4fbb99ecf..aac4a4173 100644
--- a/src/options/open_ostream.h
+++ b/src/options/open_ostream.h
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file open_ostream.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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/options/option_exception.cpp b/src/options/option_exception.cpp
index 07a8a8e57..447d3daf7 100644
--- a/src/options/option_exception.cpp
+++ b/src/options/option_exception.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file option_exception.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 Options-related exceptions
- **
- ** Options-related exceptions.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   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.
+ * ****************************************************************************
+ *
+ * Options-related exceptions.
+ */
 
 #include "options/option_exception.h"
 
diff --git a/src/options/option_exception.h b/src/options/option_exception.h
index a62fa2b80..8e5db659a 100644
--- a/src/options/option_exception.h
+++ b/src/options/option_exception.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file option_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 Options-related exceptions
- **
- ** Options-related exceptions.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * Options-related exceptions.
+ */
 
 #include "cvc4_public.h"
 
diff --git a/src/options/options.h b/src/options/options.h
index f68465a0a..8abebc253 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file options.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Paul Meng
- ** 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 Global (command-line, set-option, ...) parameters for SMT.
- **
- ** Global (command-line, set-option, ...) parameters for SMT.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Tim King, Morgan Deters, Paul Meng
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Global (command-line, set-option, ...) parameters for SMT.
+ */
 
 #include "cvc4_public.h"
 
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 2dcf26a95..2df4de4bc 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file options_handler.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 Interface for custom handlers and predicates options.
- **
- ** Interface for custom handlers and predicates options.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Interface for custom handlers and predicates options.
+ */
 
 #include "options/options_handler.h"
 
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 9b1271c8b..3e5da9ca1 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file options_handler.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Mathias Preiner, 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 Interface for custom handlers and predicates options.
- **
- ** Interface for custom handlers and predicates options.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Tim King, Mathias Preiner, 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.
+ * ****************************************************************************
+ *
+ * Interface for custom handlers and predicates options.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/options/options_holder_template.h b/src/options/options_holder_template.h
index 776bd51d6..fce0a38ac 100644
--- a/src/options/options_holder_template.h
+++ b/src/options/options_holder_template.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file options_holder_template.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Mathias Preiner, 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 Global (command-line, set-option, ...) parameters for SMT
- **
- ** Global (command-line, set-option, ...) parameters for SMT.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mathias Preiner, 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.
+ * ****************************************************************************
+ *
+ * Global (command-line, set-option, ...) parameters for SMT.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/options/options_listener.h b/src/options/options_listener.h
index e15164bfb..2c8b21e96 100644
--- a/src/options/options_listener.h
+++ b/src/options/options_listener.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file options_listener.h
- ** \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 Base class for option listener
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   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.
+ * ****************************************************************************
+ *
+ * Base class for option listener.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 3ccf3b744..f617076d5 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -1,20 +1,20 @@
-/*********************                                                        */
-/*! \file options_public_functions.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Andrew Reynolds, 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 Definitions of public facing interface functions for Options.
- **
- ** Definitions of public facing interface functions for Options. These are
- ** all 1 line wrappers for Options::get<T>, Options::set<T>, and
- ** Options::wasSetByUser<T> for different option types T.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Tim King, Gereon Kremer, 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.
+ * ****************************************************************************
+ *
+ * Definitions of public facing interface functions for Options.
+ *
+ * These are all 1 line wrappers for Options::get<T>, Options::set<T>, and
+ * Options::wasSetByUser<T> for different option types T.
+ */
 
 #include "options.h"
 
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 520cc491c..47f07db9c 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file options_template.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King, 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 Contains code for handling command-line options.
- **
- ** Contains code for handling command-line options
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * Contains code for handling command-line options.
+ */
 
 #if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)
 // force use of optreset; mingw32 croaks on argv-switching otherwise
diff --git a/src/options/printer_modes.cpp b/src/options/printer_modes.cpp
index 1ea0a3bbe..fc765db01 100644
--- a/src/options/printer_modes.cpp
+++ b/src/options/printer_modes.cpp
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file printer_modes.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Mathias Preiner, 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):
+ *   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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 #include "options/printer_modes.h"
 
diff --git a/src/options/printer_modes.h b/src/options/printer_modes.h
index d9a511903..f64ee0054 100644
--- a/src/options/printer_modes.h
+++ b/src/options/printer_modes.h
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file printer_modes.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Mathias Preiner, Andrew Reynolds, 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mathias Preiner, 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 #include "cvc4_public.h"
 
diff --git a/src/options/set_language.cpp b/src/options/set_language.cpp
index b4403f11e..0c351fb71 100644
--- a/src/options/set_language.cpp
+++ b/src/options/set_language.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file set_language.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Kshitij Bansal
- ** 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 Definition of input and output languages
- **
- ** Definition of input and output languages.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Tim King, Kshitij Bansal
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Definition of input and output languages.
+ */
 #include "options/set_language.h"
 
 #include <iosfwd>
diff --git a/src/options/set_language.h b/src/options/set_language.h
index 029ff4157..49648194f 100644
--- a/src/options/set_language.h
+++ b/src/options/set_language.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file set_language.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 Definition of input and output languages
- **
- ** Definition of input and output languages.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Definition of input and output languages.
+ */
 
 #include "cvc4_public.h"