update from the master

17 files changed, 104 insertions, 104 deletions

diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h
index 6a75bc7fa..6465a6301 100644
--- a/test/unit/util/array_store_all_black.h
+++ b/test/unit/util/array_store_all_black.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file array_store_all_black.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Black box testing of CVC4::ArrayStoreAll
  **
diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h
index bbc4d02b3..efc069246 100644
--- a/test/unit/util/assert_white.h
+++ b/test/unit/util/assert_white.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file assert_white.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief White box testing of CVC4::Configuration.
  **
diff --git a/test/unit/util/binary_heap_black.h b/test/unit/util/binary_heap_black.h
index 41e4d0e75..54241ee8e 100644
--- a/test/unit/util/binary_heap_black.h
+++ b/test/unit/util/binary_heap_black.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file binary_heap_black.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Black box testing of CVC4::BinaryHeap
  **
diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h
index b93bfafc3..0b58b1b63 100644
--- a/test/unit/util/bitvector_black.h
+++ b/test/unit/util/bitvector_black.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file bitvector_black.h
  ** \verbatim
- ** Original author: Christopher L. Conway
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Christopher L. Conway, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Black box testing of CVC4::BitVector
  **
diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h
index 4c0eb81cc..cb5e20db9 100644
--- a/test/unit/util/boolean_simplification_black.h
+++ b/test/unit/util/boolean_simplification_black.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file boolean_simplification_black.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Black box testing of CVC4::BooleanSimplification
  **
diff --git a/test/unit/util/cardinality_public.h b/test/unit/util/cardinality_public.h
index 2fcee66b6..7d7c67506 100644
--- a/test/unit/util/cardinality_public.h
+++ b/test/unit/util/cardinality_public.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file cardinality_public.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Public-box testing of CVC4::Cardinality
  **
diff --git a/test/unit/util/configuration_black.h b/test/unit/util/configuration_black.h
index f07763595..72a887f65 100644
--- a/test/unit/util/configuration_black.h
+++ b/test/unit/util/configuration_black.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file configuration_black.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Black box testing of CVC4::Configuration.
  **
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
index 91a53ddc3..d812747f5 100644
--- a/test/unit/util/datatype_black.h
+++ b/test/unit/util/datatype_black.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file datatype_black.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Andrew Reynolds
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Black box testing of CVC4::Datatype
  **
diff --git a/test/unit/util/exception_black.h b/test/unit/util/exception_black.h
index c2c7f83c0..71e99b6e4 100644
--- a/test/unit/util/exception_black.h
+++ b/test/unit/util/exception_black.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file exception_black.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Black box testing of CVC4::Exception.
  **
diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h
index 510afe7b7..563c73b66 100644
--- a/test/unit/util/integer_black.h
+++ b/test/unit/util/integer_black.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file integer_black.h
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Christopher L. Conway
+ ** Top contributors (to current version):
+ **   Tim King, Morgan Deters, Christopher L. Conway
  ** 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 Black box testing of CVC4::Integer.
  **
diff --git a/test/unit/util/integer_white.h b/test/unit/util/integer_white.h
index 12eabfbb2..b4e4129a2 100644
--- a/test/unit/util/integer_white.h
+++ b/test/unit/util/integer_white.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file integer_white.h
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief White box testing of CVC4::Integer.
  **
diff --git a/test/unit/util/listener_black.h b/test/unit/util/listener_black.h
index 682a7c67b..5319eacd1 100644
--- a/test/unit/util/listener_black.h
+++ b/test/unit/util/listener_black.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
-/*! \file output_black.h
+/*! \file listener_black.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-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 Black box testing of CVC4 output classes.
  **
@@ -137,7 +137,7 @@ public:
     }
 
     TS_ASSERT(not collection.empty());
-    for(int i=0; i < listeners.size(); ++i){
+    for(unsigned i=0; i < listeners.size(); ++i){
       ListenerCollection::Registration* at_i = listeners[i];
       delete at_i;
     }
diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h
index 369f5b673..33a0934de 100644
--- a/test/unit/util/output_black.h
+++ b/test/unit/util/output_black.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file output_black.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Black box testing of CVC4 output classes.
  **
diff --git a/test/unit/util/rational_black.h b/test/unit/util/rational_black.h
index d25c9473c..aa5e8656e 100644
--- a/test/unit/util/rational_black.h
+++ b/test/unit/util/rational_black.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file rational_black.h
  ** \verbatim
- ** Original author: Christopher L. Conway
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Christopher L. Conway, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Black box testing of CVC4::Rational.
  **
diff --git a/test/unit/util/rational_white.h b/test/unit/util/rational_white.h
index dfd0fa43b..690319b97 100644
--- a/test/unit/util/rational_white.h
+++ b/test/unit/util/rational_white.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file rational_white.h
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
+ ** Top contributors (to current version):
+ **   Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief White box testing of CVC4::Rational.
  **
diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h
index dd67429cf..c5b0d46bb 100644
--- a/test/unit/util/stats_black.h
+++ b/test/unit/util/stats_black.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file stats_black.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Kshitij Bansal
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Black box testing of CVC4::Stat and associated classes
  **
diff --git a/test/unit/util/subrange_bound_white.h b/test/unit/util/subrange_bound_white.h
index 3b785ae0d..05353aea4 100644
--- a/test/unit/util/subrange_bound_white.h
+++ b/test/unit/util/subrange_bound_white.h
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file subrange_bound_white.h
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief White-box testing of CVC4::SubrangeBound
  **