Update copyrights, add missing file-level documentation; fix perms.

120 files changed, 428 insertions, 244 deletions

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 0f5a0fd4e..1b3099842 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file approx_simplex.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
+ **/
+
 #include "cvc4autoconfig.h"
 
 #include "theory/arith/approx_simplex.h"
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index a34c8981d..b32fdef2d 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file approx_simplex.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
+ **/
+
 
 #include "cvc4_private.h"
 
diff --git a/src/theory/arith/arith_heuristic_pivot_rule.cpp b/src/theory/arith/arith_heuristic_pivot_rule.cpp
index 62b5fdff1..8a1d2b557 100644
--- a/src/theory/arith/arith_heuristic_pivot_rule.cpp
+++ b/src/theory/arith/arith_heuristic_pivot_rule.cpp
@@ -2,7 +2,7 @@
 /*! \file arith_heuristic_pivot_rule.cpp
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
+ ** Major contributors: Tim King
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/arith/arith_heuristic_pivot_rule.h b/src/theory/arith/arith_heuristic_pivot_rule.h
index 705c3e2f3..78313b81b 100644
--- a/src/theory/arith/arith_heuristic_pivot_rule.h
+++ b/src/theory/arith/arith_heuristic_pivot_rule.h
@@ -2,7 +2,7 @@
 /*! \file arith_heuristic_pivot_rule.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
+ ** Major contributors: Tim King
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 247c09294..f72537965 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -2,8 +2,8 @@
 /*! \file arith_rewriter.cpp
  ** \verbatim
  ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index bf5261439..8f6f75295 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -2,7 +2,7 @@
 /*! \file arith_static_learner.cpp
  ** \verbatim
  ** Original author: Tim King
- ** Major contributors: Dejan Jovanovic, Morgan Deters
+ ** Major contributors: Morgan Deters, Dejan Jovanovic
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 6b297f2ab..11626c1de 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -2,8 +2,8 @@
 /*! \file arith_utilities.h
  ** \verbatim
  ** Original author: Tim King
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/arith/arithvar.cpp b/src/theory/arith/arithvar.cpp
index ce05383da..d035dde2b 100644
--- a/src/theory/arith/arithvar.cpp
+++ b/src/theory/arith/arithvar.cpp
@@ -2,7 +2,7 @@
 /*! \file arithvar.cpp
  ** \verbatim
  ** Original author: Tim King
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index f0cecc24b..01137a33c 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file attempt_solution_simplex.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
+ **/
+
 
 #include "theory/arith/attempt_solution_simplex.h"
 #include "theory/arith/options.h"
diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h
index 5bcdc6aab..6e2d86f8a 100644
--- a/src/theory/arith/attempt_solution_simplex.h
+++ b/src/theory/arith/attempt_solution_simplex.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.h
+/*! \file attempt_solution_simplex.h
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): kshitij, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h
index 49c1a94ce..d3793432d 100644
--- a/src/theory/arith/bound_counts.h
+++ b/src/theory/arith/bound_counts.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index 1e827d316..d4a445b70 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file callbacks.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
+ **/
+
 #include "theory/arith/callbacks.h"
 #include "theory/arith/theory_arith_private.h"
 
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index 718799e9f..fd9369bf1 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file callbacks.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
+ **/
+
 
 #pragma once
 
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index e3e9055a7..a828b9e7f 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
+ ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index a9304ae76..b5acb9149 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.cpp
+/*! \file dual_simplex.cpp
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h
index 0ec4bc238..9d2152800 100644
--- a/src/theory/arith/dual_simplex.h
+++ b/src/theory/arith/dual_simplex.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.h
+/*! \file dual_simplex.h
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): kshitij, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index e99e62505..c0bffdf07 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.cpp
+/*! \file fc_simplex.cpp
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index 51514bcfb..2397ccdba 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.h
+/*! \file fc_simplex.h
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): kshitij, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h
index 899a3a7c6..a72ced0bc 100644
--- a/src/theory/arith/options_handlers.h
+++ b/src/theory/arith/options_handlers.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index deafb559a..c497adb75 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -2,8 +2,8 @@
 /*! \file partial_model.h
  ** \verbatim
  ** Original author: Tim King
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index d646ca889..b61cadaf8 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/arith/simplex_update.cpp b/src/theory/arith/simplex_update.cpp
index cc3b6a460..ba19d01b1 100644
--- a/src/theory/arith/simplex_update.cpp
+++ b/src/theory/arith/simplex_update.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file simplex_update.cpp
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h
index 64aa193dd..5a313e305 100644
--- a/src/theory/arith/simplex_update.h
+++ b/src/theory/arith/simplex_update.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file linear_equality.h
+/*! \file simplex_update.h
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index c0ee7ad20..2eb258d3b 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.cpp
+/*! \file soi_simplex.cpp
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index de565df64..cee6cf81d 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file simplex.h
+/*! \file soi_simplex.h
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): kshitij, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 9d06fadc4..22fbf8713 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file tableau.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
+ **/
+
 #include "theory/arith/tableau.h"
 
 using namespace std;
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index deed7e7be..3e4cb819b 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file tableau.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
+ **/
+
 #include "cvc4_private.h"
 
 #pragma once
diff --git a/src/theory/arith/tableau_sizes.cpp b/src/theory/arith/tableau_sizes.cpp
index 7c44f6791..bc0aa4dcd 100644
--- a/src/theory/arith/tableau_sizes.cpp
+++ b/src/theory/arith/tableau_sizes.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file tableau_sizes.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
+ **/
+
 #include "theory/arith/tableau_sizes.h"
 #include "theory/arith/tableau.h"
 
diff --git a/src/theory/arith/tableau_sizes.h b/src/theory/arith/tableau_sizes.h
index d6b820300..66b091fab 100644
--- a/src/theory/arith/tableau_sizes.h
+++ b/src/theory/arith/tableau_sizes.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file tableau_sizes.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
+ **/
+
 
 #include "cvc4_private.h"
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6c7f622ec..395d51d3e 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file theory_arith.cpp
  ** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): kshitij, ajreynol, mdeters, dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Original author: Tim King
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): Andrew Reynolds, Tianyi Liang, Dejan Jovanovic
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 451f1e8ff..2408094d8 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -2,8 +2,8 @@
 /*! \file theory_arith.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: Tim King
- ** Minor contributors (to current version): Andrew Reynolds, Dejan Jovanovic
+ ** Major contributors: Dejan Jovanovic, Tim King
+ ** Minor contributors (to current version): Tianyi Liang, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index aa2b2a557..002d503d0 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file theory_arith.cpp
+/*! \file theory_arith_private.cpp
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): kshitij, ajreynol, mdeters, dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): Andrew Reynolds, Tianyi Liang, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 86de3c1a9..710610346 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file theory_arith.cpp
+/*! \file theory_arith_private.h
  ** \verbatim
- ** Original author: taking
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): kshitij, ajreynol, mdeters, dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): Andrew Reynolds, Tianyi Liang, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/arith/theory_arith_private_forward.h b/src/theory/arith/theory_arith_private_forward.h
index 0dc7cdd5b..62980d83d 100644
--- a/src/theory/arith/theory_arith_private_forward.h
+++ b/src/theory/arith/theory_arith_private_forward.h
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file theory_arith_private_forward.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
+ **/
+
 
 #include "cvc4_private.h"
 
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 0d3a578a6..70f55c476 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -2,8 +2,8 @@
 /*! \file theory_arith_type_rules.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Tim King, Christopher L. Conway, Morgan Deters
- ** Minor contributors (to current version): none
+ ** Major contributors: Christopher L. Conway, Morgan Deters
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/atom_requests.cpp b/src/theory/atom_requests.cpp
index 6070004d2..b84b59d14 100644
--- a/src/theory/atom_requests.cpp
+++ b/src/theory/atom_requests.cpp
@@ -2,7 +2,7 @@
 /*! \file atom_requests.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/atom_requests.h b/src/theory/atom_requests.h
index b54ece638..689d2745b 100644
--- a/src/theory/atom_requests.h
+++ b/src/theory/atom_requests.h
@@ -2,7 +2,7 @@
 /*! \file atom_requests.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index a809ad0e8..a0179c117 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 00f183eb5..ef415139d 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -2,8 +2,8 @@
 /*! \file theory_bool_rewriter.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Tim King, Clark Barrett
- ** Minor contributors (to current version): Morgan Deters
+ ** Major contributors: Kshitij Bansal, Tim King
+ ** Minor contributors (to current version): Morgan Deters, Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
index ac9469980..ccf7deecf 100644
--- a/src/theory/booleans/theory_bool_rewriter.h
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 60199c09a..d02c9ace1 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): Andrew Reynolds
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index 19c6a9248..4a0b45d62 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: none
- ** Minor contributors (to current version): Clark Barrett, Dejan Jovanovic, Morgan Deters, lianah, Tim King
+ ** Minor contributors (to current version): Clark Barrett, Dejan Jovanovic, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 1712509b5..cbe550f96 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -2,8 +2,8 @@
 /*! \file bitblaster.cpp
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Clark Barrett, Morgan Deters, lianah
+ ** Major contributors: Dejan Jovanovic, Andrew Reynolds
+ ** Minor contributors (to current version): Clark Barrett, Kshitij Bansal, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index 6fab0369c..2dc82bddc 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -2,8 +2,8 @@
 /*! \file bitblaster.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: none
- ** Minor contributors (to current version): lianah, Morgan Deters, Dejan Jovanovic
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Kshitij Bansal, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index ccdfc1583..feb061ee1 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -2,7 +2,7 @@
 /*! \file bv_inequality_graph.cpp
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: lianah
+ ** Major contributors: none
  ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 200c49195..9a898ebe6 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /*! \file bv_inequality_graph.h
  ** \verbatim
- ** Original author: lianah
- ** Major contributors: Liana Hadarean
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 0b0551283..5a46f7a0f 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -2,8 +2,8 @@
 /*! \file bv_subtheory.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Dejan Jovanovic, lianah
- ** Minor contributors (to current version): Morgan Deters
+ ** Major contributors: Andrew Reynolds, Dejan Jovanovic
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 5a0c17134..e4b1a346d 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -2,8 +2,8 @@
 /*! \file bv_subtheory_bitblast.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: lianah
- ** Minor contributors (to current version): Liana Hadarean, Morgan Deters
+ ** Major contributors: Liana Hadarean, Clark Barrett
+ ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds, Kshitij Bansal
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index f1204dbdf..b1c1b3b66 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -2,8 +2,8 @@
 /*! \file bv_subtheory_bitblast.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters, lianah
- ** Minor contributors (to current version): Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds, Liana Hadarean, Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 6d11364d9..2433dc1ee 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -2,8 +2,8 @@
 /*! \file bv_subtheory_core.cpp
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: lianah
- ** Minor contributors (to current version): none
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index b886bbdd5..e1a73d404 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -2,8 +2,8 @@
 /*! \file bv_subtheory_core.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: lianah
- ** Minor contributors (to current version): Dejan Jovanovic
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 0eac4c035..222ba3039 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -1,9 +1,9 @@
 /*********************                                                        */
 /*! \file bv_subtheory_inequality.cpp
  ** \verbatim
- ** Original author: lianah
- ** Major contributors: Liana Hadarean
- ** Minor contributors (to current version): none
+ ** Original author: Liana Hadarean
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 6e0139e09..f142ff7be 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -1,9 +1,9 @@
 /*********************                                                        */
 /*! \file bv_subtheory_inequality.h
  ** \verbatim
- ** Original author: lianah
- ** Major contributors: none
- ** Minor contributors (to current version): Liana Hadarean
+ ** Original author: Liana Hadarean
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 7bec805ef..d137d09a0 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -1,9 +1,9 @@
 /*********************                                                        */
-/*! \file bv_to_bool.h
+/*! \file bv_to_bool.cpp
  ** \verbatim
- ** Original author: Liana Hadarean 
- ** Major contributors: None. 
- ** Minor contributors (to current version): None. 
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
index 186f2b317..b34923728 100644
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -1,9 +1,9 @@
 /*********************                                                        */
 /*! \file bv_to_bool.h
  ** \verbatim
- ** Original author: Liana Hadarean 
- ** Major contributors: None. 
- ** Minor contributors (to current version): None. 
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index e8e4ff84b..56e0a479e 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -2,8 +2,8 @@
 /*! \file slicer.cpp
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: lianah
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index fefbad756..15c0b9c0b 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -2,7 +2,7 @@
 /*! \file slicer.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: lianah
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index ce44b312d..14a19f2d0 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -2,8 +2,8 @@
 /*! \file theory_bv.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters, Liana Hadarean, lianah
- ** Minor contributors (to current version): Tim King, Andrew Reynolds, Clark Barrett
+ ** Major contributors: Morgan Deters, Liana Hadarean
+ ** Minor contributors (to current version): Tim King, Kshitij Bansal, Clark Barrett, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 708206d28..90093edfd 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -2,8 +2,8 @@
 /*! \file theory_bv.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: lianah, Dejan Jovanovic, Liana Hadarean
- ** Minor contributors (to current version): Clark Barrett, Tim King, Andrew Reynolds
+ ** Major contributors: Dejan Jovanovic, Liana Hadarean
+ ** Minor contributors (to current version): Clark Barrett, Kshitij Bansal, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 9f3d12415..db774ebe3 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: Clark Barrett
- ** Minor contributors (to current version): lianah, Morgan Deters, Tim King
+ ** Minor contributors (to current version): Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index b513dbf90..6c0ba90d4 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -2,8 +2,8 @@
 /*! \file theory_bv_rewrite_rules_operator_elimination.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Clark Barrett
- ** Minor contributors (to current version): Morgan Deters, Tim King
+ ** Major contributors: Morgan Deters, Clark Barrett
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 76eb97b39..0b09bce4d 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Liana Hadarean
- ** Minor contributors (to current version): Tim King, Morgan Deters, Clark Barrett
+ ** Minor contributors (to current version): Tim King, Clark Barrett, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index b51c56b18..12e258177 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -2,7 +2,7 @@
 /*! \file theory_bv_type_rules.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Liana Hadarean, Morgan Deters, Christopher L. Conway
+ ** Major contributors: Liana Hadarean, Christopher L. Conway, Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index ab6a615a2..5140bd498 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -2,8 +2,8 @@
 /*! \file theory_bv_utils.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: lianah, Liana Hadarean
- ** Minor contributors (to current version): Clark Barrett, Morgan Deters
+ ** Major contributors: Liana Hadarean
+ ** Minor contributors (to current version): Clark Barrett, Morgan Deters, Kshitij Bansal
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index cec1dccfc..ffd34d777 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -2,7 +2,7 @@
 /*! \file type_enumerator.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
+ ** Major contributors: Andrew Reynolds
  ** Minor contributors (to current version): Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/decision_attributes.h b/src/theory/decision_attributes.h
index 79f58feb1..fa934ecc7 100644
--- a/src/theory/decision_attributes.h
+++ b/src/theory/decision_attributes.h
@@ -2,7 +2,7 @@
 /*! \file decision_attributes.h
  ** \verbatim
  ** Original author: Kshitij Bansal
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/idl/idl_assertion.cpp b/src/theory/idl/idl_assertion.cpp
index 1e725932b..717122195 100644
--- a/src/theory/idl/idl_assertion.cpp
+++ b/src/theory/idl/idl_assertion.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/idl/idl_assertion.h b/src/theory/idl/idl_assertion.h
index 8ce0e93b2..d0328e600 100644
--- a/src/theory/idl/idl_assertion.h
+++ b/src/theory/idl/idl_assertion.h
@@ -2,7 +2,7 @@
 /*! \file idl_assertion.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/idl/idl_assertion_db.cpp b/src/theory/idl/idl_assertion_db.cpp
index 697c70c02..692084071 100644
--- a/src/theory/idl/idl_assertion_db.cpp
+++ b/src/theory/idl/idl_assertion_db.cpp
@@ -2,7 +2,7 @@
 /*! \file idl_assertion_db.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/idl/idl_assertion_db.h b/src/theory/idl/idl_assertion_db.h
index 0501bc6bf..205102b0f 100644
--- a/src/theory/idl/idl_assertion_db.h
+++ b/src/theory/idl/idl_assertion_db.h
@@ -2,7 +2,7 @@
 /*! \file idl_assertion_db.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/idl/idl_model.cpp b/src/theory/idl/idl_model.cpp
index 75f4834ea..71cd44314 100644
--- a/src/theory/idl/idl_model.cpp
+++ b/src/theory/idl/idl_model.cpp
@@ -2,7 +2,7 @@
 /*! \file idl_model.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/idl/idl_model.h b/src/theory/idl/idl_model.h
index 64407684b..22e05c469 100644
--- a/src/theory/idl/idl_model.h
+++ b/src/theory/idl/idl_model.h
@@ -2,7 +2,7 @@
 /*! \file idl_model.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
index e5100fc71..987973bf3 100644
--- a/src/theory/idl/theory_idl.cpp
+++ b/src/theory/idl/theory_idl.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_idl.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h
index c629ad2b0..4597d4c6a 100644
--- a/src/theory/idl/theory_idl.h
+++ b/src/theory/idl/theory_idl.h
@@ -2,7 +2,7 @@
 /*! \file theory_idl.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: none
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
index facd5f4f0..1b4e096f2 100644
--- a/src/theory/ite_utilities.cpp
+++ b/src/theory/ite_utilities.cpp
@@ -1,9 +1,9 @@
 /*********************                                                        */
-/*! \file ite_simplifier.cpp
+/*! \file ite_utilities.cpp
  ** \verbatim
- ** Original author: Clark Barrett
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h
index 73f0386d2..d9e6120aa 100644
--- a/src/theory/ite_utilities.h
+++ b/src/theory/ite_utilities.h
@@ -1,9 +1,9 @@
 /*********************                                                        */
-/*! \file ite_simplifier.h
+/*! \file ite_utilities.h
  ** \verbatim
- ** Original author: Clark Barrett
+ ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 080550a16..28485a979 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -2,6 +2,8 @@
 /*! \file bounded_integers.cpp
  ** \verbatim
  ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index 3da938d31..972bdb2ec 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -1,13 +1,16 @@
 /*********************                                                        */
 /*! \file bounded_integers.h
-** \verbatim
-** Original author: Andrew Reynolds
-** This file is part of the CVC4 project.
-** Copyright (c) 2009-2013  New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief This class manages integer bounds for quantifiers
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
 **/
 
 #include "cvc4_private.h"
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 42b49cf01..783f6284d 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -2,7 +2,7 @@
 /*! \file candidate_generator.cpp
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
+ ** Major contributors: Andrew Reynolds
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index 402a29848..a87c24596 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -2,7 +2,7 @@
 /*! \file candidate_generator.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
+ ** Major contributors: Andrew Reynolds
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index fa4961352..bda124e96 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -2,8 +2,8 @@
 /*! \file first_order_model.cpp
  ** \verbatim
  ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp
index ebfb55f08..a696af3c2 100644
--- a/src/theory/quantifiers/first_order_reasoning.cpp
+++ b/src/theory/quantifiers/first_order_reasoning.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file first_order_reasoning.cpp
  ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h
index 5f217050c..6bc5c21c1 100644
--- a/src/theory/quantifiers/first_order_reasoning.h
+++ b/src/theory/quantifiers/first_order_reasoning.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file first_order_reasoning.h
  ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index c22d903f9..2f32ec5e6 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -2,6 +2,8 @@
 /*! \file full_model_check.cpp
  ** \verbatim
  ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index abe05d3c7..606392831 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -2,6 +2,8 @@
 /*! \file full_model_check.h
  ** \verbatim
  ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 4fe4072a3..6cc446e35 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Andrew Reynolds
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 821beeae0..c70c90b29 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Andrew Reynolds
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index b079ae75c..b079ae75c 100755..100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index c4345f828..c4345f828 100755..100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 107a99014..441ab029c 100755..100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -1,7 +1,9 @@
 /*********************                                                        */
-/*! \file bounded_integers.cpp
+/*! \file rewrite_engine.cpp
  ** \verbatim
  ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 2d9d751c2..a9a2f9b46 100755..100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -1,13 +1,16 @@
 /*********************                                                        */
-/*! \file bounded_integers.h
-** \verbatim
-** Original author: Andrew Reynolds
-** This file is part of the CVC4 project.
-** Copyright (c) 2009-2013  New York University and The University of Iowa
-** See the file COPYING in the top-level source directory for licensing
-** information.\endverbatim
-**
-** \brief This class manages integer bounds for quantifiers
+/*! \file rewrite_engine.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
 **/
 
 #include "cvc4_private.h"
diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp
index 507a50838..66a3ac79f 100755..100644
--- a/src/theory/quantifiers/symmetry_breaking.cpp
+++ b/src/theory/quantifiers/symmetry_breaking.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file symmetry_breaking.cpp
  ** \verbatim
- ** Original author: ajreynol
+ ** Original author: Andrew Reynolds
  ** Major contributors: none
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h
index 7f6855fea..d7d9e0f6f 100755..100644
--- a/src/theory/quantifiers/symmetry_breaking.h
+++ b/src/theory/quantifiers/symmetry_breaking.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
 /*! \file symmetry_breaking.h
  ** \verbatim
- ** Original author: ajreynol
+ ** Original author: Andrew Reynolds
  ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 066282c2c..e72242fe9 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -2,8 +2,8 @@
 /*! \file theory_quantifiers.cpp
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic, Andrew Reynolds
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index e9a69bd30..e9a69bd30 100755..100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index f9add4fac..f12184869 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Clark Barrett
+ ** Minor contributors (to current version): Liana Hadarean, Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 24f09e62d..f88de72f9 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index 17aed4e42..aa2964e13 100644
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -2,7 +2,7 @@
 /*! \file rewriter_tables_template.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters
+ ** Major contributors: Morgan Deters, Tim King
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/rewriterules/theory_rewriterules_rewriter.h b/src/theory/rewriterules/theory_rewriterules_rewriter.h
index f49471407..511ef3515 100644
--- a/src/theory/rewriterules/theory_rewriterules_rewriter.h
+++ b/src/theory/rewriterules/theory_rewriterules_rewriter.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index f26037cf0..e7079081b 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -1,14 +1,14 @@
-/*********************                                                        */

-/*! \file regexp_operation.CPP

- ** \verbatim

- ** Original author: Tianyi Liang

- ** Major contributors: Tianyi Liang, Andrew Reynolds

- ** Minor contributors (to current version): none

- ** This file is part of the CVC4 prototype.

- ** Copyright (c) 2013-2013  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

+/*********************                                                        */
+/*! \file regexp_operation.cpp
+ ** \verbatim
+ ** Original author: Tianyi Liang
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
  ** \brief Regular Expresion Operations

  **

  ** Regular Expresion Operations

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 702e5ba84..a47f7bd77 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -1,14 +1,14 @@
-/*********************                                                        */

-/*! \file regexp_operation.h

- ** \verbatim

- ** Original author: Tianyi Liang

- ** Major contributors: Tianyi Liang, Andrew Reynolds

- ** Minor contributors (to current version): none

- ** This file is part of the CVC4 prototype.

- ** Copyright (c) 2013-2013  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

+/*********************                                                        */
+/*! \file regexp_operation.h
+ ** \verbatim
+ ** Original author: Tianyi Liang
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
  ** \brief Regular Expresion Operations

  **

  ** Regular Expresion Operations

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9a88883fc..9f4d84765 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2,10 +2,10 @@
 /*! \file theory_strings.cpp
  ** \verbatim
  ** Original author: Tianyi Liang
- ** Major contributors: Tianyi Liang, Andrew Reynolds
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 9fae67a9f..4d2a192cf 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -4,8 +4,8 @@
  ** Original author: Tianyi Liang
  ** Major contributors: none
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index c54cbb3b2..9da0e343d 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -2,10 +2,10 @@
 /*! \file theory_strings_preprocess.cpp
  ** \verbatim
  ** Original author: Tianyi Liang
- ** Major contributors: Tianyi Liang, Andrew Reynolds
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 7bc60c1a1..698ef6ba1 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -2,10 +2,10 @@
 /*! \file theory_strings_preprocess.h
  ** \verbatim
  ** Original author: Tianyi Liang
- ** Major contributors: Tianyi Liang, Andrew Reynolds
+ ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 73f17a146..cd9db85c7 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -4,8 +4,8 @@
  ** Original author: Tianyi Liang
  ** Major contributors: none
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 78f0da59e..318176297 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -4,8 +4,8 @@
  ** Original author: Tianyi Liang
  ** Major contributors: none
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 080d6abf5..d5019ab39 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -4,8 +4,8 @@
  ** Original author: Tianyi Liang
  ** Major contributors: none
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2013-2013  New York University and The University of Iowa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index af4dea293..7cf4d7ad9 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Christopher L. Conway, Kshitij Bansal, Tim King, Liana Hadarean, Clark Barrett, Andrew Reynolds
+ ** Minor contributors (to current version): Christopher L. Conway, Kshitij Bansal, Liana Hadarean, Clark Barrett, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e5b2ad8d2..ffc36e59b 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Christopher L. Conway, Francois Bobot, Kshitij Bansal, Liana Hadarean, Clark Barrett, Tim King, Andrew Reynolds
+ ** Minor contributors (to current version): Christopher L. Conway, Francois Bobot, Kshitij Bansal, Clark Barrett, Liana Hadarean, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 73ff068b4..4f753187f 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /*! \file theory_model.cpp
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters, Clark Barrett
+ ** Original author: Morgan Deters
+ ** Major contributors: Andrew Reynolds, Clark Barrett
  ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 9da9cb5e2..598db2683 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /*! \file theory_model.h
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters, Clark Barrett
+ ** Original author: Morgan Deters
+ ** Major contributors: Andrew Reynolds, Clark Barrett
  ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/theory_registrar.h b/src/theory/theory_registrar.h
index d77bf1eb0..691c1147b 100644
--- a/src/theory/theory_registrar.h
+++ b/src/theory/theory_registrar.h
@@ -2,7 +2,7 @@
 /*! \file theory_registrar.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Tim King, Morgan Deters
+ ** Major contributors: Morgan Deters, Tim King
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 199581b98..cb44b42df 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: none
- ** Minor contributors (to current version): Tim King, Francois Bobot, Morgan Deters
+ ** Minor contributors (to current version): Dejan Jovanovic, Tim King, Francois Bobot, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index a9294dc69..ab106bc8d 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Tim King, Liana Hadarean, Andrew Reynolds
+ ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Liana Hadarean, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index bf41a256d..409b41e3f 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Andrew Reynolds
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Clark Barrett
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 40713fa41..3bd316c93 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Dejan Jovanovic
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 50a746205..b4d1b6d48 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -2,8 +2,8 @@
 /*! \file theory_uf_type_rules.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Christopher L. Conway, Morgan Deters
- ** Minor contributors (to current version): Andrew Reynolds, Tim King
+ ** Major contributors: Christopher L. Conway, Andrew Reynolds, Morgan Deters
+ ** Minor contributors (to current version): Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 8bbdded3e..a6e885f97 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Clark Barrett
  ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Minor contributors (to current version): Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h
index 0ee754256..d41c7db5d 100644
--- a/src/theory/unconstrained_simplifier.h
+++ b/src/theory/unconstrained_simplifier.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Clark Barrett
  ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Minor contributors (to current version): Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing