update from the master

18 files changed, 110 insertions, 110 deletions

diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp
index f21037628..247131cce 100644
--- a/examples/api/bitvectors.cpp
+++ b/examples/api/bitvectors.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file bitvectors.cpp
  ** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A simple demonstration of the solving capabilities of the CVC4
  ** bit-vector solver.
diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp
index 14135fc90..83100a815 100644
--- a/examples/api/bitvectors_and_arrays.cpp
+++ b/examples/api/bitvectors_and_arrays.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file bitvectors_and_arrays.cpp
  ** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A simple demonstration of the solving capabilities of the CVC4
  ** bit-vector and array solvers.
diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index 5ae0e207e..f9b18f707 100644
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file combination.cpp
  ** \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 A simple demonstration of the capabilities of CVC4
  **
diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp
index 3da8cfa4a..14aab16c9 100644
--- a/examples/api/datatypes.cpp
+++ b/examples/api/datatypes.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file datatypes.cpp
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief An example of using inductive datatypes in CVC4
  **
diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp
index fac242b76..98a75c8a8 100644
--- a/examples/api/extract.cpp
+++ b/examples/api/extract.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
-/*! \file bitvectors.cpp
+/*! \file extract.cpp
  ** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Clark Barrett, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A simple demonstration of the solving capabilities of the CVC4
  ** bit-vector solver.
diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp
index b94c46318..b4ce34503 100644
--- a/examples/api/helloworld.cpp
+++ b/examples/api/helloworld.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file helloworld.cpp
  ** \verbatim
- ** Original author: Tim King
- ** Major contributors: Kshitij Bansal
- ** Minor contributors (to current version): Morgan Deters
+ ** Top contributors (to current version):
+ **   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 A very simple CVC4 example
  **
diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java
index 42250a399..5def97e0d 100644
--- a/examples/api/java/BitVectors.java
+++ b/examples/api/java/BitVectors.java
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file BitVectors.java
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A simple demonstration of the solving capabilities of the CVC4
  ** bit-vector solver.
diff --git a/examples/api/java/BitVectorsAndArrays.java b/examples/api/java/BitVectorsAndArrays.java
index aa13726c8..97cf7e857 100644
--- a/examples/api/java/BitVectorsAndArrays.java
+++ b/examples/api/java/BitVectorsAndArrays.java
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file BitVectorsAndArrays.java
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A simple demonstration of the solving capabilities of the CVC4
  ** bit-vector and array solvers.
diff --git a/examples/api/java/CVC4Streams.java b/examples/api/java/CVC4Streams.java
index 9c8bad688..343a576e3 100644
--- a/examples/api/java/CVC4Streams.java
+++ b/examples/api/java/CVC4Streams.java
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file CVC4Streams.java
  ** \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 Example of driving CVC4 parsing from Java streams
  **
diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java
index 1d98a4ac0..199e85709 100644
--- a/examples/api/java/Combination.java
+++ b/examples/api/java/Combination.java
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file Combination.java
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A simple demonstration of the capabilities of CVC4
  **
diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java
index d38f5738a..c1ae770ef 100644
--- a/examples/api/java/Datatypes.java
+++ b/examples/api/java/Datatypes.java
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file Datatypes.java
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief An example of using inductive datatypes in CVC4 (Java version)
  **
diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java
index 7674a8e88..5cedc6321 100644
--- a/examples/api/java/HelloWorld.java
+++ b/examples/api/java/HelloWorld.java
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file HelloWorld.java
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A very simple CVC4 example
  **
diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java
index 271e08ad9..3cb9f7926 100644
--- a/examples/api/java/LinearArith.java
+++ b/examples/api/java/LinearArith.java
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file LinearArith.java
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A simple demonstration of the linear arithmetic capabilities of CVC4
  **
diff --git a/examples/api/java/PipedInput.java b/examples/api/java/PipedInput.java
index b393ca33f..88622aa05 100644
--- a/examples/api/java/PipedInput.java
+++ b/examples/api/java/PipedInput.java
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file PipedInput.java
  ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief A simple demonstration of the input parsing capabilities of CVC4
  ** when used from Java
diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java
index bb9dcd822..4f09ca8f4 100644
--- a/examples/api/java/Strings.java
+++ b/examples/api/java/Strings.java
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file Strings.java
  ** \verbatim
- ** Original author: Tianyi Liang
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Clark Barrett, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Reasoning about strings with CVC4 via Java API.
  **
diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp
index 22d65ad10..cd180f290 100644
--- a/examples/api/linear_arith.cpp
+++ b/examples/api/linear_arith.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file linear_arith.cpp
  ** \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 A simple demonstration of the linear arithmetic capabilities of CVC4
  **
diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index 68de230fe..bb7deeac6 100644
--- a/examples/api/sets.cpp
+++ b/examples/api/sets.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file sets.cpp
  ** \verbatim
- ** Original author: Kshitij Bansal
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Kshitij Bansal, 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 Reasoning about sets with CVC4.
  **
diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp
index 2e5d467d3..d8350d011 100644
--- a/examples/api/strings.cpp
+++ b/examples/api/strings.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
-/*! \file sets.cpp
+/*! \file strings.cpp
  ** \verbatim
- ** Original author: Tianyi Liang
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ **   Clark Barrett, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief Reasoning about strings with CVC4 via C++ API.
  **