Refactor and update copyright headers. (#6316)

77 files changed, 1106 insertions, 1058 deletions

diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index 804a93401..7e29e4849 100644
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file abduction_solver.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, 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 The solver for abduction queries
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * The solver for abduction queries.
+ */
 
 #include "smt/abduction_solver.h"
 
diff --git a/src/smt/abduction_solver.h b/src/smt/abduction_solver.h
index eee6f52cd..e8a97c043 100644
--- a/src/smt/abduction_solver.h
+++ b/src/smt/abduction_solver.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file abduction_solver.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, 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 The solver for abduction queries
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * The solver for abduction queries.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/abstract_values.cpp b/src/smt/abstract_values.cpp
index fc978d39b..81c7af16b 100644
--- a/src/smt/abstract_values.cpp
+++ b/src/smt/abstract_values.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file abstract_values.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   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 Utility for constructing and maintaining abstract values.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   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.
+ * ****************************************************************************
+ *
+ * Utility for constructing and maintaining abstract values.
+ */
 
 #include "smt/abstract_values.h"
 
diff --git a/src/smt/abstract_values.h b/src/smt/abstract_values.h
index 125be2511..843adbb22 100644
--- a/src/smt/abstract_values.h
+++ b/src/smt/abstract_values.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file abstract_values.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, 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 Utility for constructing and maintaining abstract values.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * Utility for constructing and maintaining abstract values.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index bfb14e2c4..d873f31bb 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file assertions.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
- ** 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 The module for storing assertions for an SMT engine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The module for storing assertions for an SMT engine.
+ */
 
 #include "smt/assertions.h"
 
diff --git a/src/smt/assertions.h b/src/smt/assertions.h
index 157d063f4..3603c0df6 100644
--- a/src/smt/assertions.h
+++ b/src/smt/assertions.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file assertions.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The module for storing assertions for an SMT engine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Morgan Deters, Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The module for storing assertions for an SMT engine.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index b84bc3e64..ebc8f46a1 100644
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file check_models.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Utility for constructing and maintaining abstract values.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Morgan Deters, Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Utility for constructing and maintaining abstract values.
+ */
 
 #include "smt/check_models.h"
 
diff --git a/src/smt/check_models.h b/src/smt/check_models.h
index 997857515..f2c7b50ba 100644
--- a/src/smt/check_models.h
+++ b/src/smt/check_models.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file check_models.h
- ** \verbatim
- ** Top contributors (to current version):
- **   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 Utility for checking models
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * Utility for checking models.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index a8d9afdfa..5585ab48f 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file command.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Abdalrhman Mohamed, 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 Implementation of command objects.
- **
- ** Implementation of command objects.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Tim King, Abdalrhman Mohamed, 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.
+ * ****************************************************************************
+ *
+ * Implementation of command objects.
+ */
 
 #include "smt/command.h"
 
diff --git a/src/smt/command.h b/src/smt/command.h
index d28c0975d..9ef09abec 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1,21 +1,21 @@
-/*********************                                                        */
-/*! \file command.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Abdalrhman Mohamed, Tim King, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implementation of the command pattern on SmtEngines.
- **
- ** Implementation of the command pattern on SmtEngines.  Command
- ** objects are generated by the parser (typically) to implement the
- ** commands in parsed input (see Parser::parseNextCommand()), or by
- ** client code.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Abdalrhman Mohamed, 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.
+ * ****************************************************************************
+ *
+ * Implementation of the command pattern on SmtEngines.
+ *
+ * Command objects are generated by the parser (typically) to implement the
+ * commands in parsed input (see Parser::parseNextCommand()), or by client
+ * code.
+ */
 
 #include "cvc4_public.h"
 
diff --git a/src/smt/defined_function.h b/src/smt/defined_function.h
index 6ad0b73c7..ab225b095 100644
--- a/src/smt/defined_function.h
+++ b/src/smt/defined_function.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file defined_function.h
- ** \verbatim
- ** Top contributors (to current version):
- **   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 Defined function data structure
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   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.
+ * ****************************************************************************
+ *
+ * Defined function data structure.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index 73f26dc92..f5ebd3c5b 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file dump.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli, 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 Dump utility classes and functions
- **
- ** Dump utility classes and functions.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli, 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.
+ * ****************************************************************************
+ *
+ * Dump utility classes and functions.
+ */
 
 #include "smt/dump.h"
 
diff --git a/src/smt/dump.h b/src/smt/dump.h
index 6e14fc59f..a56529fe3 100644
--- a/src/smt/dump.h
+++ b/src/smt/dump.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file dump.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Andres Noetzli, Abdalrhman Mohamed
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Dump utility classes and functions
- **
- ** Dump utility classes and functions.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Andres Noetzli, Abdalrhman Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Dump utility classes and functions.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp
index 4b7f0b056..83ff8e6b9 100644
--- a/src/smt/dump_manager.cpp
+++ b/src/smt/dump_manager.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file dump_manager.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Gereon Kremer, 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 Implementation of the dump manager.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Gereon Kremer, 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.
+ * ****************************************************************************
+ *
+ * Implementation of the dump manager.
+ */
 
 #include "smt/dump_manager.h"
 
diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
index 2b1644bef..de9a8ba2e 100644
--- a/src/smt/dump_manager.h
+++ b/src/smt/dump_manager.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file dump_manager.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, 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 The dump manager of the SmtEngine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * The dump manager of the SmtEngine.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index e88710628..38e93f38e 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -1,17 +1,18 @@
-/*********************                                                        */
-/*! \file env.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Smt Environment, main access to global utilities available to
- ** internal code.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Gereon Kremer, 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.
+ * ****************************************************************************
+ *
+ * Smt Environment, main access to global utilities available to
+ * internal code.
+ */
 
 #include "smt/env.h"
 
diff --git a/src/smt/env.h b/src/smt/env.h
index c22044338..d13cd7a71 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -1,17 +1,18 @@
-/*********************                                                        */
-/*! \file env.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 Smt Environment, main access to global utilities available to
- ** internal code
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * Smt Environment, main access to global utilities available to
+ * internal code
+ */
 
 #include "cvc4_public.h"
 
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index 59597b97f..0c5cf6ad5 100644
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file expand_definitions.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implementation of expand definitions for an SMT engine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Andres Noetzli, Aina Niemetz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of expand definitions for an SMT engine.
+ */
 
 #include "smt/expand_definitions.h"
 
diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index a3d70542b..7a05d6a3a 100644
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file expand_definitions.h
- ** \verbatim
- ** Top contributors (to current version):
- **   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 The module for processing assertions for an SMT engine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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 module for processing assertions for an SMT engine.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index 7b75ea2ed..48d81a91f 100644
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file interpolation_solver.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Ying Sheng, Andrew Reynolds, Abdalrhman Mohamed
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The solver for interpolation queries
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Ying Sheng, Andrew Reynolds, Aina Niemetz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The solver for interpolation queries.
+ */
 
 #include "smt/interpolation_solver.h"
 
diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h
index 62f469970..e5480e6dc 100644
--- a/src/smt/interpolation_solver.h
+++ b/src/smt/interpolation_solver.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file interpolation_solver.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Ying Sheng, 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 The solver for interpolation queries
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Ying Sheng, 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.
+ * ****************************************************************************
+ *
+ * The solver for interpolation queries.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index e7ea9bb40..a3c271fc5 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file listeners.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Abdalrhman Mohamed
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implements listener classes for SMT engine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Abdalrhman Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implements listener classes for SMT engine.
+ */
 
 #include "smt/listeners.h"
 
diff --git a/src/smt/listeners.h b/src/smt/listeners.h
index 2ca8b8ad8..afc81c047 100644
--- a/src/smt/listeners.h
+++ b/src/smt/listeners.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file listeners.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Abdalrhman Mohamed, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Listener classes for SMT engine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Abdalrhman Mohamed, Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Listener classes for SMT engine.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h
index e9f747313..df08b5734 100644
--- a/src/smt/logic_exception.h
+++ b/src/smt/logic_exception.h
@@ -1,21 +1,19 @@
-/*********************                                                        */
-/*! \file logic_exception.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, 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 a feature is used outside
- ** the logic that CVC4 is currently using
- **
- ** \brief An exception that is thrown when a feature is used outside
- ** the logic that CVC4 is currently using (for example, a quantifier
- ** is used while running in a quantifier-free logic).
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, 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.
+ * ****************************************************************************
+ *
+ * An exception that is thrown when a feature is used outside
+ * the logic that CVC4 is currently using (for example, a quantifier
+ * is used while running in a quantifier-free logic).
+ */
 
 #include "cvc4_public.h"
 
diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp
index 6962ef495..b0f9aef21 100644
--- a/src/smt/managed_ostreams.cpp
+++ b/src/smt/managed_ostreams.cpp
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file managed_ostreams.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, 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 Wrappers to handle memory management of ostreams.
- **
- ** This file contains wrappers to handle special cases of managing memory
- ** related to ostreams.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Tim King, 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.
+ * ****************************************************************************
+ *
+ * Wrappers to handle memory management of ostreams.
+ *
+ * This file contains wrappers to handle special cases of managing memory
+ * related to ostreams.
+ */
 
 #include "smt/managed_ostreams.h"
 
diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h
index 9737979ea..d519fc826 100644
--- a/src/smt/managed_ostreams.h
+++ b/src/smt/managed_ostreams.h
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file managed_ostreams.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Mathias Preiner, Gereon Kremer
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Wrappers to handle memory management of ostreams.
- **
- ** This file contains wrappers to handle special cases of managing memory
- ** related to ostreams.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Tim King, Mathias Preiner, Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Wrappers to handle memory management of ostreams.
+ *
+ * This file contains wrappers to handle special cases of managing memory
+ * related to ostreams.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/model.cpp b/src/smt/model.cpp
index a3742b652..cf6a90f12 100644
--- a/src/smt/model.cpp
+++ b/src/smt/model.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file model.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, 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 implementation of Model class
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * Implementation of Model class.
+ */
 
 #include "smt/model.h"
 
diff --git a/src/smt/model.h b/src/smt/model.h
index 1dd65a6b9..b6d0b1644 100644
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file model.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, 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 Model class
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * Model class.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
index 64769a2ad..04613f848 100644
--- a/src/smt/model_blocker.cpp
+++ b/src/smt/model_blocker.cpp
@@ -1,17 +1,17 @@
-/*********************                                                        */
-/*! \file model_blocker.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   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 Implementation of utility for blocking models.
- **
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * Implementation of utility for blocking models.
+ */
 
 #include "smt/model_blocker.h"
 
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
index 6ef9b0662..a6a8ea31d 100644
--- a/src/smt/model_blocker.h
+++ b/src/smt/model_blocker.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file model_blocker.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner, Gereon Kremer
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Utility for blocking the current model
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Mathias Preiner, Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Utility for blocking the current model.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp
index f16c93e62..5b6df3c1a 100644
--- a/src/smt/model_core_builder.cpp
+++ b/src/smt/model_core_builder.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file model_core_builder.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   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 Implementation of utility for building model cores
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * Implementation of utility for building model cores.
+ */
 
 #include "smt/model_core_builder.h"
 
diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h
index 05e9b804e..fac456484 100644
--- a/src/smt/model_core_builder.h
+++ b/src/smt/model_core_builder.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file model_core_builder.h
- ** \verbatim
- ** Top contributors (to current version):
- **   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 Utility for building model cores
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   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.
+ * ****************************************************************************
+ *
+ * Utility for building model cores.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp
index 61d380b72..b3e747ecb 100644
--- a/src/smt/node_command.cpp
+++ b/src/smt/node_command.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file node_command.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Abdalrhman Mohamed, Yoni Zohar, 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 Implementation of NodeCommand functions.
- **
- ** Implementation of NodeCommand functions.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Abdalrhman Mohamed, Yoni Zohar, 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.
+ * ****************************************************************************
+ *
+ * Implementation of NodeCommand functions.
+ */
 
 #include "smt/node_command.h"
 
diff --git a/src/smt/node_command.h b/src/smt/node_command.h
index 87bb713c6..af59bb195 100644
--- a/src/smt/node_command.h
+++ b/src/smt/node_command.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file node_command.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Abdalrhman Mohamed
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Datastructures used for printing commands internally.
- **
- ** Datastructures used for printing commands internally.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Abdalrhman Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Datastructures used for printing commands internally.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index 70fa0f28c..f854ec402 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file optimization_solver.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Michael Chang, Yancheng Ou
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The solver for optimization queries
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Michael Chang, Yancheng Ou, Aina Niemetz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The solver for optimization queries.
+ */
 
 #include "smt/optimization_solver.h"
 
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
index edbbcbde1..9d075e5de 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file optimization_solver.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Michael Chang, Yancheng Ou
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The solver for optimization queries
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Michael Chang, Yancheng Ou, Aina Niemetz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The solver for optimization queries.
+ */
 
 #include "cvc4_private.h"
 
@@ -70,7 +71,7 @@ enum class OptResult
  * - the optimization target node,
  * - whether it's maximize/minimize
  * - and whether it's signed for BitVectors
- **/
+ */
 class Objective
 {
  public:
diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp
index 0a7a0c54a..2c732fa9d 100644
--- a/src/smt/options_manager.cpp
+++ b/src/smt/options_manager.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file options_manager.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, 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 Module for managing options of an SmtEngine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Aina Niemetz
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Module for managing options of an SmtEngine.
+ */
 
 #include "smt/options_manager.h"
 
diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h
index 89f5acd6a..4705b4273 100644
--- a/src/smt/options_manager.h
+++ b/src/smt/options_manager.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file options_manager.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, 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 Module for managing options of an SmtEngine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Tim King, Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Module for managing options of an SmtEngine.
+ */
 
 #ifndef CVC5__SMT__OPTIONS_MANAGER_H
 #define CVC5__SMT__OPTIONS_MANAGER_H
diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp
index a01c7a6a9..6395a4c2c 100644
--- a/src/smt/output_manager.cpp
+++ b/src/smt/output_manager.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file output_manager.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Abdalrhman Mohamed
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implementation of OutputManager functions.
- **
- ** Implementation of OutputManager functions.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Abdalrhman Mohamed, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of OutputManager functions.
+ */
 
 #include "smt/output_manager.h"
 
diff --git a/src/smt/output_manager.h b/src/smt/output_manager.h
index 668daae0b..bb7645f75 100644
--- a/src/smt/output_manager.h
+++ b/src/smt/output_manager.h
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file output_manager.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Abdalrhman Mohamed
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The output manager for the SmtEngine.
- **
- ** The output manager provides helper functions for printing commands
- ** internally.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Abdalrhman Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The output manager for the SmtEngine.
+ *
+ * The output manager provides helper functions for printing commands
+ * internally.
+ */
 
 #ifndef CVC5__SMT__OUTPUT_MANAGER_H
 #define CVC5__SMT__OUTPUT_MANAGER_H
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index 016f60cfc..ea5d28a23 100644
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -1,17 +1,18 @@
-/*********************                                                        */
-/*! \file preprocess_proof_generator.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   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 The implementation of the module for proofs for preprocessing in an
- ** SMT engine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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 implementation of the module for proofs for preprocessing in an
+ * SMT engine.
+ */
 
 #include "smt/preprocess_proof_generator.h"
 
diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index a9d5bd2b6..1bd03d7f5 100644
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file preprocess_proof_generator.h
- ** \verbatim
- ** Top contributors (to current version):
- **   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 The module for proofs for preprocessing in an SMT engine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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 module for proofs for preprocessing in an SMT engine.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 28f393704..859eb84fc 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file preprocessor.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The preprocessor of the SMT engine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * The preprocessor of the SMT engine.
+ */
 
 #include "smt/preprocessor.h"
 
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 40b1b1278..e0fa39593 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file preprocessor.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Justin Xu
- ** 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 The preprocessor of the SmtEngine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Morgan Deters, Justin Xu
+ *
+ * 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 preprocessor of the SmtEngine.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 29651211c..2c97d9413 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file process_assertions.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Yoni Zohar
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implementation of module for processing assertions for an SMT engine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * Implementation of module for processing assertions for an SMT engine.
+ */
 
 #include "smt/process_assertions.h"
 
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index e3f5ae3a3..5931899d9 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file process_assertions.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The module for processing assertions for an SMT engine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Gereon Kremer, 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.
+ * ****************************************************************************
+ *
+ * The module for processing assertions for an SMT engine.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 549f10008..b06590918 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file proof_manager.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Haniel Barbosa, 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 The proof manager of the SMT engine
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Haniel Barbosa, Diego Della Rocca de Camargos
+ *
+ * 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 proof manager of the SMT engine.
+ */
 
 #include "smt/proof_manager.h"
 
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index 32f3f73d9..0345991d2 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file proof_manager.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Gereon Kremer, Haniel Barbosa
- ** 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 The proof manager of SmtEngine
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Gereon Kremer, Haniel Barbosa
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The proof manager of SmtEngine.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 19ca089d3..105376719 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file proof_post_processor.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Haniel Barbosa
- ** 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 module for processing proof nodes
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Haniel Barbosa, 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.
+ * ****************************************************************************
+ *
+ * Implementation of module for processing proof nodes.
+ */
 
 #include "smt/proof_post_processor.h"
 
diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index 2459270c0..f5379290e 100644
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file proof_post_processor.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Haniel Barbosa
- ** 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 The module for processing proof nodes
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Haniel Barbosa, 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 module for processing proof nodes.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index 436d6618d..2f9b89d06 100644
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file quant_elim_solver.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   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 The solver for quantifier elimination queries
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * The solver for quantifier elimination queries.
+ */
 
 #include "smt/quant_elim_solver.h"
 
diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h
index cf3be1ec3..06f12ced9 100644
--- a/src/smt/quant_elim_solver.h
+++ b/src/smt/quant_elim_solver.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file quant_elim_solver.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 The solver for quantifier elimination queries
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * The solver for quantifier elimination queries.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 6a5ed52d0..0a8819c4b 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file set_defaults.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
- ** 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 setting default options.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of setting default options.
+ */
 
 #include "smt/set_defaults.h"
 
diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h
index d3d82774c..6e77b488c 100644
--- a/src/smt/set_defaults.h
+++ b/src/smt/set_defaults.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file set_defaults.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 Method for setting the default options of an SMT engine.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Method for setting the default options of an SMT engine.
+ */
 
 #ifndef CVC5__SMT__SET_DEFAULTS_H
 #define CVC5__SMT__SET_DEFAULTS_H
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bb14232bb..3a67b7bf3 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file smt_engine.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The main entry point into the CVC4 library's SMT interface
- **
- ** The main entry point into the CVC4 library's SMT interface.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The main entry point into the cvc5 library's SMT interface.
+ */
 
 #include "smt/smt_engine.h"
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index df5c69613..63ba5f831 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file smt_engine.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, 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 SmtEngine: the main public entry point of libcvc4.
- **
- ** SmtEngine: the main public entry point of libcvc4.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * SmtEngine: the main public entry point of libcvc5.
+ */
 
 #include "cvc4_public.h"
 
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index aa349d980..1164bc1b5 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file smt_engine_scope.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli, Morgan Deters, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli, 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 #include "smt/smt_engine_scope.h"
 
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index e00c4fcb1..46efac90a 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file smt_engine_scope.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Andres Noetzli, 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):
+ *   Andrew Reynolds, Andres Noetzli, 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_private.h"
 
diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index c8f23f7f8..cabaf8823 100644
--- a/src/smt/smt_engine_state.cpp
+++ b/src/smt/smt_engine_state.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file smt_engine_state.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Ying Sheng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Utility for maintaining the state of the SMT engine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Morgan Deters, Ying Sheng
+ *
+ * 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 for maintaining the state of the SMT engine.
+ */
 
 #include "smt/smt_engine_state.h"
 
diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h
index 0e02a5605..284771cc5 100644
--- a/src/smt/smt_engine_state.h
+++ b/src/smt/smt_engine_state.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file smt_engine_state.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Ying Sheng, Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Utility for maintaining the state of the SMT engine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Ying Sheng, 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.
+ * ****************************************************************************
+ *
+ * Utility for maintaining the state of the SMT engine.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp
index b0de2d8b3..5147c046a 100644
--- a/src/smt/smt_engine_stats.cpp
+++ b/src/smt/smt_engine_stats.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file smt_engine_stats.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, 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 Implementation of statistics for SMT engine
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Implementation of statistics for SMT engine.
+ */
 
 #include "smt/smt_engine_stats.h"
 
diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h
index b3fd5a1b7..fa95709d8 100644
--- a/src/smt/smt_engine_stats.h
+++ b/src/smt/smt_engine_stats.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file smt_engine_stats.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, 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 Statistics for SMT engine
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * Statistics for SMT engine.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/smt_mode.cpp b/src/smt/smt_mode.cpp
index db21e53c4..2ac8bcdea 100644
--- a/src/smt/smt_mode.cpp
+++ b/src/smt/smt_mode.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file smt_mode.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Enumeration type for the mode of an SmtEngine.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Enumeration type for the mode of an SmtEngine.
+ */
 
 #include "smt/smt_mode.h"
 
diff --git a/src/smt/smt_mode.h b/src/smt/smt_mode.h
index 47cb15eb6..8061a2e21 100644
--- a/src/smt/smt_mode.h
+++ b/src/smt/smt_mode.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file smt_mode.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Ying Sheng, 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 Enumeration type for the mode of an SmtEngine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Ying Sheng, 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.
+ * ****************************************************************************
+ *
+ * Enumeration type for the mode of an SmtEngine.
+ */
 
 #include "cvc4_public.h"
 
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 3a1c6b12c..fbb679cf7 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file smt_solver.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, 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 The solver for SMT queries in an SmtEngine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * The solver for SMT queries in an SmtEngine.
+ */
 
 #include "smt/smt_solver.h"
 
diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index 06f576445..e4493eedf 100644
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file smt_solver.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, 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 The solver for SMT queries in an SmtEngine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, 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.
+ * ****************************************************************************
+ *
+ * The solver for SMT queries in an SmtEngine.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/smt_statistics_registry.cpp b/src/smt/smt_statistics_registry.cpp
index dd5ed470c..db437526a 100644
--- a/src/smt/smt_statistics_registry.cpp
+++ b/src/smt/smt_statistics_registry.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file smt_statistics_registry.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 Accessor for the SmtEngine's StatisticsRegistry.
- **
- ** Accessor for the SmtEngine's StatisticsRegistry.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Accessor for the SmtEngine's StatisticsRegistry.
+ */
 
 #include "smt/smt_statistics_registry.h"
 
diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h
index 97bdde703..cafb9e62a 100644
--- a/src/smt/smt_statistics_registry.h
+++ b/src/smt/smt_statistics_registry.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file smt_statistics_registry.h
- ** \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 Accessor for the SmtEngine's StatisticsRegistry.
- **
- ** Accessor for the SmtEngine's StatisticsRegistry.
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Accessor for the SmtEngine's StatisticsRegistry.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 022691a12..00598534f 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file sygus_solver.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The solver for sygus queries
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The solver for SyGuS queries.
+ */
 
 #include "smt/sygus_solver.h"
 
diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h
index 8e6f08b75..f701419d9 100644
--- a/src/smt/sygus_solver.h
+++ b/src/smt/sygus_solver.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file sygus_solver.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The solver for sygus queries
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The solver for SyGuS queries.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 262c46870..823511b02 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file term_formula_removal.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Dejan Jovanovic, Mudathir Mohamed
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Removal of term formulas
- **
- ** Removal of term formulas.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Dejan Jovanovic, Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Removal of term formulas.
+ */
 #include "smt/term_formula_removal.h"
 
 #include <vector>
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index d2d3bf6fd..65f4bdb7a 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -1,18 +1,17 @@
-/*********************                                                        */
-/*! \file term_formula_removal.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Dejan Jovanovic, 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 Removal of term formulas
- **
- ** Removal of term formulas.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Dejan Jovanovic, 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.
+ * ****************************************************************************
+ *
+ * Removal of term formulas.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp
index 976e7ea6c..df8f2f9d9 100644
--- a/src/smt/unsat_core_manager.cpp
+++ b/src/smt/unsat_core_manager.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file unsat_core_manager.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Haniel Barbosa
- ** 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 the unsat core manager of SmtEngine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Haniel Barbosa
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of the unsat core manager of SmtEngine.
+ */
 
 #include "unsat_core_manager.h"
 
diff --git a/src/smt/unsat_core_manager.h b/src/smt/unsat_core_manager.h
index ac87bbe6e..6bfcec9f8 100644
--- a/src/smt/unsat_core_manager.h
+++ b/src/smt/unsat_core_manager.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file unsat_core_manager.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Haniel Barbosa
- ** 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 The unsat core manager of SmtEngine.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Haniel Barbosa
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The unsat core manager of SmtEngine.
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h
index b1cb855c6..8bb230982 100644
--- a/src/smt/update_ostream.h
+++ b/src/smt/update_ostream.h
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file update_ostream.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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
 
 #include "cvc4_private.h"
 
diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp
index 2ae39a664..c7e3d3280 100644
--- a/src/smt/witness_form.cpp
+++ b/src/smt/witness_form.cpp
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file witness_form.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief The module for managing witness form conversion in proofs
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * The module for managing witness form conversion in proofs.
+ */
 
 #include "smt/witness_form.h"
 
diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h
index 37f672e57..938fc40d1 100644
--- a/src/smt/witness_form.h
+++ b/src/smt/witness_form.h
@@ -1,16 +1,17 @@
-/*********************                                                        */
-/*! \file witness_form.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 The module for managing witness form conversion in proofs
- **/
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * The module for managing witness form conversion in proofs.
+ */
 
 #include "cvc4_private.h"