Updating the copyright headers and scripts.

27 files changed, 164 insertions, 164 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 1adc71d70..40b757598 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file boolean_terms.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ]]
  **
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
index e1865f29f..0a63f7fd8 100644
--- a/src/smt/boolean_terms.h
+++ b/src/smt/boolean_terms.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file boolean_terms.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ]]
  **
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 5bf74a7de..bd514e2a8 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file command.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Francois Bobot
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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.
  **
diff --git a/src/smt/command.h b/src/smt/command.h
index 7c9706522..db4efd819 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file command.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Christopher L. Conway, Dejan Jovanovic, Francois Bobot, Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Francois Bobot
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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.
  **
diff --git a/src/smt/command_list.cpp b/src/smt/command_list.cpp
index 2319d9539..78e5914aa 100644
--- a/src/smt/command_list.cpp
+++ b/src/smt/command_list.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file command_list.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A context-sensitive list of Commands, and their cleanup
  **
diff --git a/src/smt/command_list.h b/src/smt/command_list.h
index 47185b365..ea6b64940 100644
--- a/src/smt/command_list.h
+++ b/src/smt/command_list.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file command_list.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A context-sensitive list of Commands, and their cleanup
  **
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index 79bf43e3c..eee7b901a 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file dump.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King, Morgan Deters, Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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
  **
diff --git a/src/smt/dump.h b/src/smt/dump.h
index a6fa899da..2abfe5408 100644
--- a/src/smt/dump.h
+++ b/src/smt/dump.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file dump.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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
  **
diff --git a/src/smt/ite_removal.cpp b/src/smt/ite_removal.cpp
index c0c6ed02b..fcd0c3254 100644
--- a/src/smt/ite_removal.cpp
+++ b/src/smt/ite_removal.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file ite_removal.cpp
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Tim King, Morgan Deters
- ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett
+ ** Top contributors (to current version):
+ **   Morgan Deters, Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ITEs
  **
diff --git a/src/smt/ite_removal.h b/src/smt/ite_removal.h
index d6d820f89..c0a46c316 100644
--- a/src/smt/ite_removal.h
+++ b/src/smt/ite_removal.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file ite_removal.h
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Kshitij Bansal, Tim King, Morgan Deters
- ** Minor contributors (to current version): Clark Barrett
+ ** Top contributors (to current version):
+ **   Morgan Deters, Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ITEs
  **
diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h
index a641f8d21..93db29a9b 100644
--- a/src/smt/logic_exception.h
+++ b/src/smt/logic_exception.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file logic_exception.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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
diff --git a/src/smt/logic_request.cpp b/src/smt/logic_request.cpp
index 09559eb8d..dc6a2d6b7 100644
--- a/src/smt/logic_request.cpp
+++ b/src/smt/logic_request.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file logic_request.cpp
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ]]
  **
diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h
index 94c6c2a5e..7b41886bd 100644
--- a/src/smt/logic_request.h
+++ b/src/smt/logic_request.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file logic_request.h
  ** \verbatim
- ** Original author: Martin Brain <>
- ** Major contributors: none
- ** Minor contributors (to current version): Tim King
+ ** Top contributors (to current version):
+ **   Martin Brain, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 object to request logic widening in the running SmtEngine
  **
diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp
index 1901f731d..cae6ac67f 100644
--- a/src/smt/managed_ostreams.cpp
+++ b/src/smt/managed_ostreams.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file managed_ostreams.cpp
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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.
  **
diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h
index 6dc785027..56c517a87 100644
--- a/src/smt/managed_ostreams.h
+++ b/src/smt/managed_ostreams.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file managed_ostreams.h
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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.
  **
diff --git a/src/smt/model.cpp b/src/smt/model.cpp
index 15ecbadfb..a38862307 100644
--- a/src/smt/model.cpp
+++ b/src/smt/model.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file model.cpp
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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
  **/
diff --git a/src/smt/model.h b/src/smt/model.h
index 4bbcb5f7d..768cb3e6a 100644
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file model.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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
  **/
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index aa645954b..369c5d48f 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file model_postprocessor.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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
  **
diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h
index 024f4f3a3..d9e749677 100644
--- a/src/smt/model_postprocessor.h
+++ b/src/smt/model_postprocessor.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file model_postprocessor.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 
  **
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 784d82228..ddbb9eef7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file smt_engine.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Clark Barrett
- ** Minor contributors (to current version): Christopher L. Conway, Tianyi Liang, Martin Brain <>, Kshitij Bansal, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Morgan Deters, Clark Barrett, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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
  **
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 0a8f8099f..2741cea85 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file smt_engine.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Martin Brain <>, Tim King, Clark Barrett, Christopher L. Conway, Andrew Reynolds, Kshitij Bansal, Dejan Jovanovic
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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.
  **
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index 1712744d7..a58102d86 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file smt_engine_check_proof.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Guy Katz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ]]
  **
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index 25004c85e..c31ea5736 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file smt_engine_scope.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ]]
  **
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 5a7e39849..e00be40d4 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file smt_engine_scope.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ]]
  **
diff --git a/src/smt/smt_statistics_registry.cpp b/src/smt/smt_statistics_registry.cpp
index 5aa9085f5..d34498697 100644
--- a/src/smt/smt_statistics_registry.cpp
+++ b/src/smt/smt_statistics_registry.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
-/*! \file smt_statistic_registry.cpp
+/*! \file smt_statistics_registry.cpp
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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.
  **
diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h
index 60a5e7c53..7483e8215 100644
--- a/src/smt/smt_statistics_registry.h
+++ b/src/smt/smt_statistics_registry.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
-/*! \file smt_statistic_registry.h
+/*! \file smt_statistics_registry.h
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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.
  **
diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h
index b87ed69d2..9574c5460 100644
--- a/src/smt/update_ostream.h
+++ b/src/smt/update_ostream.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file update_ostream.h
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the 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 ]]
  **