Copyright text fixes.

2 files changed, 49 insertions, 22 deletions

diff --git a/AUTHORS b/AUTHORS
index 8db72131b..24cb5327a 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -1,17 +1,27 @@
-The core authors and designers of CVC4 are:
-
-  Kshitij Bansal <kshitij@cs.nyu.edu>, New York University
-  Clark Barrett <barrett@cs.nyu.edu>, New York University
-  Francois Bobot <bobot@lri.fr>, Commissariat a l'Energie Atomique (CEA)
-  Martin Brain <martin.brain@cs.ox.ac.uk>, University of Oxford
-  Christopher Conway <cconway@cs.nyu.edu>, Google
-  Morgan Deters <mdeters@cs.nyu.edu>, New York University
-  Liana Hadarean <lianah@cs.nyu.edu>, New York University
-  Dejan Jovanovic <dejan@cs.nyu.edu>, SRI International
-  Tim King <taking@cs.nyu.edu>, New York University
-  Tianyi Liang <tianyi-liang@uiowa.edu>, The University of Iowa
-  Andrew Reynolds <andrew.j.reynolds@gmail.com>, EPFL
-  Cesare Tinelli <tinelli@cs.uiowa.edu>, The University of Iowa
+The authors, designers, and main contributors to CVC4 are listed below.
+CVC4's copyright is held by these individuals and the affiliated
+institutions at the time of their contributions (see the file COPYING).
+All rights reserved.
+
+The core designers and authors of CVC4 are:
+
+  Kshitij Bansal, New York University
+  Clark Barrett, New York University
+  Francois Bobot, The University of Iowa & Commissariat a l'Energie Atomique
+  Martin Brain, University of Oxford
+  Christopher Conway, formerly at New York University
+  Morgan Deters, New York University
+  Liana Hadarean, New York University and Mentor Graphics Corporation
+  Dejan Jovanovic, New York University & SRI International
+  Tim King, formerly at New York University
+  Tianyi Liang, The University of Iowa
+  Andrew Reynolds, The University of Iowa & EPFL
+  Cesare Tinelli, The University of Iowa
+
+Chief contributors to the CVC4 codebase additionally include:
+
+  Peter Collingbourne, formerly in the Multicore Programming Group at
+    Imperial College London (headed by Alastair Donaldson)
 
 CVC4 is the fourth in the CVC series of tools (CVC, CVC Lite, CVC3) but does
 not directly incorporate code from any previous version.  Information about
diff --git a/COPYING b/COPYING
index dddf4ed59..6785f5b88 100644
--- a/COPYING
+++ b/COPYING
@@ -1,15 +1,32 @@
-CVC4 is copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 New York University
-and The University of Iowa.  All rights reserved.
+CVC4 is copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 by its authors
+and contributors (see the file AUTHORS) and their institutional
+affiliations.  All rights reserved.
 
 The source code of CVC4 is open and available to students, researchers,
 software companies, and everyone else to study, to modify, and to
 redistribute original or modified versions; distribution is under the
-terms of the modified BSD license.  However, CVC4 can be configured (and
-is, by default) to link against some GPLed libraries, and therefore the
-use of these builds may be restricted in non-GPL-compatible projects.
-See below for a discussion of CLN, GLPK, and Readline (the three GPLed
-optional library dependences for CVC4), and how to ensure you have a
-build that doesn't link against GPLed libraries.
+terms of the modified BSD license (reproduced below).  However, CVC4
+can be configured (however, by default it is not) to link against some
+GPLed libraries, and therefore the use of these builds may be restricted
+in non-GPL-compatible projects.  See below for a discussion of CLN, GLPK,
+and Readline (the three GPLed optional library dependences for CVC4),
+and how to ensure you have a build that doesn't link against GPLed
+libraries.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its
+   contributors may be used to endorse or promote products derived from
+   this software without specific prior written permission.
 
 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
 ''AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT