Use new copyright header format.

20 files changed, 120 insertions, 130 deletions

diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp
index e74d83882..434ff3d24 100644
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/antlr_input_imports.cpp
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file antlr_input_imports.cpp
  ** \verbatim
- ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   none 
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index b5bad6a2d..368a6db82 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -489,10 +489,11 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 
 @header {
 /**
- ** This file is part of CVC4.
- ** 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.
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.
  **/
 }/* @header */
 
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index 28c54fc80..c7548db71 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -31,10 +31,11 @@ options {
 
 @header {
 /**
- ** This file is part of CVC4.
- ** 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.
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.
  **/
 }/* @header */
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 1b96d9bd3..01b2ab7da 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -31,10 +31,11 @@ options {
 
 @header {
 /**
- ** This file is part of CVC4.
- ** 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.
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.
  **/
 }/* @header */
 
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index dcee52337..6f1af9c74 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -32,10 +32,11 @@ options {
 
 @header {
 /**
- ** This file is part of CVC4.
- ** 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.
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.
  **/
 }/* @header */
 
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 368a79b80..95f8dca5b 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file bvminisat.cpp
  ** \verbatim
- ** Original author: dejan
- ** Major contributors:
- ** Minor contributors (to current version):
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   none 
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief SAT Solver.
  **
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 732bd0313..1a9ee3f96 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file bvminisat.h
  ** \verbatim
- ** Original author: dejan
- ** Major contributors:
- ** Minor contributors (to current version):
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   none 
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief SAT Solver.
  **
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index eff079cc9..efd3cd5cc 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file cryptominisat.cpp
  ** \verbatim
- ** Original author: lianah
- ** Major contributors:
- ** Minor contributors (to current version):
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   none 
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief SAT Solver.
  **
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index 7ad861def..c3f5edbb1 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file cryptominisat.h
  ** \verbatim
- ** Original author: lianah
- ** Major contributors:
- ** Minor contributors (to current version):
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   none 
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief SAT Solver.
  **
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index a88a872c8..f7a8f22cb 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file minisat.cpp
  ** \verbatim
- ** Original author: dejan
- ** Major contributors:
- ** Minor contributors (to current version):
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   none 
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief SAT Solver.
  **
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 1627a6575..d649ad894 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -1,15 +1,13 @@
 /*********************                                                        */
 /*! \file minisat.h
  ** \verbatim
- ** Original author: dejan
- ** Major contributors:
- ** Minor contributors (to current version):
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ **   none 
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief SAT Solver.
  **
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 9d064d74d..4c6cd3eb4 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_sep.cpp
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Implementation of the theory of sep.
  **
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 8dd1ed356..00e67f5ff 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_sep.h
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Dejan Jovanovic, Clark Barrett
- ** Minor contributors (to current version): Tim King, Andrew Reynolds
+ ** Top 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Theory of sep
  **
diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index 0faf7b176..2e6a54ebd 100644
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_sep_rewriter.cpp
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
diff --git a/src/theory/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h
index 58b79c7fd..c71248319 100644
--- a/src/theory/sep/theory_sep_rewriter.h
+++ b/src/theory/sep/theory_sep_rewriter.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_sep_rewriter.h
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h
index 0eae782c8..8de0783e2 100644
--- a/src/theory/sep/theory_sep_type_rules.h
+++ b/src/theory/sep/theory_sep_type_rules.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_sep_type_rules.h
  ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Typing and cardinality rules for the theory of sep
  **
diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h
index df14bf53b..9863b9734 100644
--- a/src/theory/sets/rels_utils.h
+++ b/src/theory/sets/rels_utils.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file rels_utils.h
  ** \verbatim
- ** Original author: Paul Meng
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Sets theory implementation.
  **
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 03e0c64f8..5f9243b33 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_sets_rels.cpp
  ** \verbatim
- ** Original author: Paul Meng
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Sets theory implementation.
  **
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 576430eb1..24c744203 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_sets_rels.h
  ** \verbatim
- ** Original author: Paul Meng
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top 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
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Sets theory implementation.
  **
diff --git a/src/util/channel.h b/src/util/channel.h
index 39aed425b..5a5610410 100644
--- a/src/util/channel.h
+++ b/src/util/channel.h
@@ -1,9 +1,8 @@
 /*********************                                                        */
 /*! \file channel.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   none 
  ** This file is part of the CVC4 project but is excluded from the
  ** standard CVC4 licensing because it is a derivative work of
  ** circular_buffer.hpp in the BOOST 1.46.1 distribution.
@@ -13,6 +12,7 @@
  ** The combined work is:
  **   Copyright (c) 2009-2014  New York University and The University of Iowa
  **   Copyright (c) 2003-2008  Jan Gaspar
+ ** \endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **