Update copyrights.

88 files changed, 151 insertions, 100 deletions

diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp
index 3ed372848..d99353b74 100644
--- a/src/util/abstract_value.cpp
+++ b/src/util/abstract_value.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h
index 39fd9e368..78a1e9975 100644
--- a/src/util/abstract_value.h
+++ b/src/util/abstract_value.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/array.h b/src/util/array.h
index 892e28a86..ab554171f 100644
--- a/src/util/array.h
+++ b/src/util/array.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/array_store_all.cpp b/src/util/array_store_all.cpp
index 7c9086276..dfd021e75 100644
--- a/src/util/array_store_all.cpp
+++ b/src/util/array_store_all.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/array_store_all.h b/src/util/array_store_all.h
index 6e60cc2cb..bccefdd58 100644
--- a/src/util/array_store_all.h
+++ b/src/util/array_store_all.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/ascription_type.h b/src/util/ascription_type.h
index 1f7ba0aaa..42906e557 100644
--- a/src/util/ascription_type.h
+++ b/src/util/ascription_type.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/backtrackable.h b/src/util/backtrackable.h
index 57ed94771..5492dd8b5 100644
--- a/src/util/backtrackable.h
+++ b/src/util/backtrackable.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h
index e666611a4..53c2a9bb6 100644
--- a/src/util/bin_heap.h
+++ b/src/util/bin_heap.h
@@ -2,7 +2,7 @@
 /*! \file bin_heap.h
  ** \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-2014  New York University and The University of Iowa
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 35b052531..798dd63c7 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -5,7 +5,7 @@
  ** Major contributors: Morgan Deters, Liana Hadarean
  ** Minor contributors (to current version): Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
  **
diff --git a/src/util/bool.h b/src/util/bool.h
index 373b4fdec..2d5e15777 100644
--- a/src/util/bool.h
+++ b/src/util/bool.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/boolean_simplification.cpp b/src/util/boolean_simplification.cpp
index 8e077fe1d..62ef46339 100644
--- a/src/util/boolean_simplification.cpp
+++ b/src/util/boolean_simplification.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h
index be39f69c1..d0ca3646f 100644
--- a/src/util/boolean_simplification.h
+++ b/src/util/boolean_simplification.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/cache.h b/src/util/cache.h
index 8c2f9abca..5183c439b 100644
--- a/src/util/cache.h
+++ b/src/util/cache.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index 42f8519c1..dfee0aae2 100644
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: 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
+ ** 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
  **
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 34aa9c08b..524d9cda4 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -5,7 +5,7 @@
  ** Major contributors: 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
+ ** 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
  **
diff --git a/src/util/chain.h b/src/util/chain.h
index e9216724e..e052a2ed8 100644
--- a/src/util/chain.h
+++ b/src/util/chain.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/channel.h b/src/util/channel.h
index 676371cbc..3644f786a 100644
--- a/src/util/channel.h
+++ b/src/util/channel.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/cvc4_assert.cpp b/src/util/cvc4_assert.cpp
index 08e2867f6..3db285182 100644
--- a/src/util/cvc4_assert.cpp
+++ b/src/util/cvc4_assert.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/cvc4_assert.h b/src/util/cvc4_assert.h
index 7d359a56b..cc854278b 100644
--- a/src/util/cvc4_assert.h
+++ b/src/util/cvc4_assert.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): ACSYS
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
  **
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index f0ddc2cf6..9e07c746a 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/datatype.h b/src/util/datatype.h
index befb3428d..32fae8235 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -2,10 +2,10 @@
 /*! \file datatype.h
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Andrew Reynolds
+ ** 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
+ ** 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
  **
diff --git a/src/util/debug.h b/src/util/debug.h
index 97c176f02..6ef196111 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/dense_map.h b/src/util/dense_map.h
index 10ca9f72f..39cee5b9e 100644
--- a/src/util/dense_map.h
+++ b/src/util/dense_map.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic
+ ** 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
+ ** 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
  **
diff --git a/src/util/didyoumean_test.cpp b/src/util/didyoumean_test.cpp
index 2fe3331d9..0c46d5ffe 100644
--- a/src/util/didyoumean_test.cpp
+++ b/src/util/didyoumean_test.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file didyoumean_test.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** 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
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 // Compile: g++ didyoumean_test.cpp didyoumean.cpp
 // For debug compile with -DDIDYOUMEAN_DEBUG or -DDIDYOUMEAN_DEBUG1 or both
 
diff --git a/src/util/divisible.cpp b/src/util/divisible.cpp
index 4e20d6b5f..ee085d25b 100644
--- a/src/util/divisible.cpp
+++ b/src/util/divisible.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/divisible.h b/src/util/divisible.h
index 0c0c7bc5b..6917bf2a6 100644
--- a/src/util/divisible.h
+++ b/src/util/divisible.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/dump.cpp b/src/util/dump.cpp
index e3baf10c5..53c5eae6a 100644
--- a/src/util/dump.cpp
+++ b/src/util/dump.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/dump.h b/src/util/dump.h
index a85062af1..2cf5877d4 100644
--- a/src/util/dump.h
+++ b/src/util/dump.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/dynamic_array.h b/src/util/dynamic_array.h
index 1f6e07cc7..18b1b645b 100644
--- a/src/util/dynamic_array.h
+++ b/src/util/dynamic_array.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/emptyset.cpp b/src/util/emptyset.cpp
index fa1bb8f10..7905f11fb 100644
--- a/src/util/emptyset.cpp
+++ b/src/util/emptyset.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file emptyset.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** 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
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
 #include "util/emptyset.h"
 #include <iostream>
 
diff --git a/src/util/emptyset.h b/src/util/emptyset.h
index 43a868e42..4b3bb204f 100644
--- a/src/util/emptyset.h
+++ b/src/util/emptyset.h
@@ -2,7 +2,7 @@
 /*! \file emptyset.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-2014  New York University and The University of Iowa
diff --git a/src/util/exception.cpp b/src/util/exception.cpp
index 08405c501..ab510c27d 100644
--- a/src/util/exception.cpp
+++ b/src/util/exception.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/exception.h b/src/util/exception.h
index cd4b763ef..937729f0c 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
index b5654e9cb..d3f0d09d4 100644
--- a/src/util/gmp_util.h
+++ b/src/util/gmp_util.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/hash.h b/src/util/hash.h
index 0cdc96fcb..218cf0aab 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/index.h b/src/util/index.h
index be3e2918b..ea0802b2d 100644
--- a/src/util/index.h
+++ b/src/util/index.h
@@ -5,7 +5,7 @@
  ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
  **
diff --git a/src/util/integer.h.in b/src/util/integer.h.in
index c3c6a70cd..3db9998a7 100644
--- a/src/util/integer.h.in
+++ b/src/util/integer.h.in
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index bd23b48c9..02086494b 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -1,3 +1,20 @@
+/*********************                                                        */
+/*! \file integer_cln_imp.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-2014  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 "util/integer.h"
 #include <string>
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 8b56c4b19..9f7f4a06b 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -5,7 +5,7 @@
  ** Major contributors: Morgan Deters
  ** Minor contributors (to current version): Dejan Jovanovic, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
  **
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index bb6166523..2717d03f4 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -2,10 +2,10 @@
 /*! \file integer_gmp_imp.cpp
  ** \verbatim
  ** Original author: Tim King
- ** Major contributors: Morgan Deters, Christopher L. Conway
+ ** 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
+ ** 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
  **
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 68d335aec..d1f5050d5 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -5,7 +5,7 @@
  ** Major contributors: Morgan Deters, Liana Hadarean
  ** 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
+ ** 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
  **
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index f1dce413c..68d7d9a34 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -2,10 +2,10 @@
 /*! \file ite_removal.cpp
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters, Andrew Reynolds, Tim King
- ** Minor contributors (to current version): Clark Barrett
+ ** Major contributors: Tim King, Morgan Deters
+ ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
  **
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index de5f83f27..83c55dab7 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -2,10 +2,10 @@
 /*! \file ite_removal.h
  ** \verbatim
  ** Original author: Dejan Jovanovic
- ** Major contributors: Kshitij Bansal, Morgan Deters, Tim King
- ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett
+ ** Major contributors: Kshitij Bansal, Tim King, Morgan Deters
+ ** 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
+ ** 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
  **
diff --git a/src/util/language.cpp b/src/util/language.cpp
index 1a184e648..f19f20c03 100644
--- a/src/util/language.cpp
+++ b/src/util/language.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): Francois Bobot
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
  **
diff --git a/src/util/language.h b/src/util/language.h
index 0d1c5486a..be962bf3e 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): Francois Bobot
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
  **
diff --git a/src/util/lemma_input_channel.h b/src/util/lemma_input_channel.h
index 319de942c..44f0b87f5 100644
--- a/src/util/lemma_input_channel.h
+++ b/src/util/lemma_input_channel.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/lemma_output_channel.h b/src/util/lemma_output_channel.h
index 8f4f7461d..df7abd1e9 100644
--- a/src/util/lemma_output_channel.h
+++ b/src/util/lemma_output_channel.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/matcher.h b/src/util/matcher.h
index 4a3233261..107891a54 100644
--- a/src/util/matcher.h
+++ b/src/util/matcher.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/maybe.h b/src/util/maybe.h
index b1c81f76e..4d279a0c7 100644
--- a/src/util/maybe.h
+++ b/src/util/maybe.h
@@ -3,9 +3,9 @@
  ** \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
+ ** 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
  **
diff --git a/src/util/model.cpp b/src/util/model.cpp
index e25065c21..c1254ab47 100644
--- a/src/util/model.cpp
+++ b/src/util/model.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/model.h b/src/util/model.h
index 1d80b0308..98794a53d 100644
--- a/src/util/model.h
+++ b/src/util/model.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/nary_builder.cpp b/src/util/nary_builder.cpp
index 08aceef6f..d89121fd7 100644
--- a/src/util/nary_builder.cpp
+++ b/src/util/nary_builder.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/nary_builder.h b/src/util/nary_builder.h
index 7676cadbc..c98e01b1b 100644
--- a/src/util/nary_builder.h
+++ b/src/util/nary_builder.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h
index 1d2bf0b9d..66a58efd1 100644
--- a/src/util/node_visitor.h
+++ b/src/util/node_visitor.h
@@ -5,7 +5,7 @@
  ** Major contributors: Liana Hadarean, 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
+ ** 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
  **
diff --git a/src/util/ntuple.h b/src/util/ntuple.h
index a342a11c1..b9e1100f1 100644
--- a/src/util/ntuple.h
+++ b/src/util/ntuple.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/output.cpp b/src/util/output.cpp
index d60330b0c..462043805 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/output.h b/src/util/output.h
index 7394f24ab..0974591db 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): Tim King, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
  **
diff --git a/src/util/predicate.cpp b/src/util/predicate.cpp
index 1b473d5ad..787d329aa 100644
--- a/src/util/predicate.cpp
+++ b/src/util/predicate.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/predicate.h b/src/util/predicate.h
index 5fb3f806a..5ead2f090 100644
--- a/src/util/predicate.h
+++ b/src/util/predicate.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/proof.h b/src/util/proof.h
index aa81d3294..be1e2a8e2 100644
--- a/src/util/proof.h
+++ b/src/util/proof.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/rational.h.in b/src/util/rational.h.in
index c02886906..6f9c29c19 100644
--- a/src/util/rational.h.in
+++ b/src/util/rational.h.in
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index f674481de..e5e3608cb 100644
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: Morgan Deters, Christopher L. Conway
  ** 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
+ ** 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
  **
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index b144ab419..895fc1c9b 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
index 25c7dab59..155faebf2 100644
--- a/src/util/rational_gmp_imp.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: Morgan Deters, Christopher L. Conway
  ** 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
+ ** 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
  **
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index 273b3072d..6288be050 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/record.cpp b/src/util/record.cpp
index 136f190a1..ea9b5495a 100644
--- a/src/util/record.cpp
+++ b/src/util/record.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/record.h b/src/util/record.h
index 63c54930e..5689a4209 100644
--- a/src/util/record.h
+++ b/src/util/record.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h
index a4177f600..3369c5c23 100644
--- a/src/util/recursion_breaker.h
+++ b/src/util/recursion_breaker.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index ce6f0d29b..b1b454cfa 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -2,10 +2,10 @@
 /*! \file regexp.cpp
  ** \verbatim
  ** Original author: Tianyi Liang
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** 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
+ ** 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
  **
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 9f522bdaa..e75ca1fad 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/result.cpp b/src/util/result.cpp
index 909a7d8c6..91b671262 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: 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
+ ** 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
  **
diff --git a/src/util/result.h b/src/util/result.h
index 21bf563bd..8c804daa7 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -5,7 +5,7 @@
  ** Major contributors: 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
+ ** 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
  **
diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index 52d992d4b..64b898d45 100644
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 0222382b0..a121b5195 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -5,7 +5,7 @@
  ** Major contributors: Tim King, 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
+ ** 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
  **
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index 90382c365..179bb1a23 100644
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Andrew Reynolds
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
  **
diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h
index 4cf2ab732..4bb1a072e 100644
--- a/src/util/sort_inference.h
+++ b/src/util/sort_inference.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index d632933b4..ff31e7b4b 100644
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/statistics.h b/src/util/statistics.h
index 5b9e75837..a7088f5c5 100644
--- a/src/util/statistics.h
+++ b/src/util/statistics.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 61762b84d..097869bc7 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -2,10 +2,10 @@
 /*! \file statistics_registry.cpp
  ** \verbatim
  ** Original author: Morgan Deters
- ** Major contributors: Tim King
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): Kshitij Bansal, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
  **
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 186433c5a..b9e3eaf8b 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -3,9 +3,9 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Tim King
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** 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
  **
diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h
index 82dc940ea..b90656f33 100644
--- a/src/util/subrange_bound.h
+++ b/src/util/subrange_bound.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/tls.h.in b/src/util/tls.h.in
index e13149c3a..88969e250 100644
--- a/src/util/tls.h.in
+++ b/src/util/tls.h.in
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp
index 970d2542e..02b51d751 100644
--- a/src/util/trans_closure.cpp
+++ b/src/util/trans_closure.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h
index 14e7ab95f..27f32377e 100644
--- a/src/util/trans_closure.h
+++ b/src/util/trans_closure.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/tuple.h b/src/util/tuple.h
index 375a1aba3..fe016db2c 100644
--- a/src/util/tuple.h
+++ b/src/util/tuple.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/uninterpreted_constant.cpp b/src/util/uninterpreted_constant.cpp
index 6b98a7be8..f0d9a42d2 100644
--- a/src/util/uninterpreted_constant.cpp
+++ b/src/util/uninterpreted_constant.cpp
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/uninterpreted_constant.h b/src/util/uninterpreted_constant.h
index 869491538..c4fb776bc 100644
--- a/src/util/uninterpreted_constant.h
+++ b/src/util/uninterpreted_constant.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **
diff --git a/src/util/utility.h b/src/util/utility.h
index 9b15adecd..59522901a 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -5,7 +5,7 @@
  ** 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
+ ** 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
  **