A few updates to license files.

diff --git a/COPYING b/COPYING
index 1cd650bec52f6092a726fd10989d17ca95b2319b..bd00768009631db929d58e229eb28bded515129a 100644 (file)
--- a/COPYING
+++ b/COPYING
@@ -1,5 +1,5 @@
-CVC4 is copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 by its
-authors and contributors (see the file AUTHORS) and their institutional
+CVC4 is copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017 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,
@@ -218,11 +218,14 @@ Their copyright:
   (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
   THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 
-CVC4 links against The GNU Multiple Precision Arithmetic Library. It is
-licensed under GNU LGPL v3. See GMP-LICENSE for a copy of the license.
+CVC4 by default links against The GNU Multiple Precision (GMP) Arithmetic
+Library, which is licensed under GNU LGPL v3. See the file GMP-LICENSE for a
+copy of that license.  Note that according to the terms of the LGPL, both
+CVC4's source, and the combined work (CVC4 linked with GMP) may (and do) remain
+under the more permissive CVC4 license.
 
-CVC4 can be optionally configured to link against CLN, the Class Library for
-Numbers, available here:
+Alternatively, CVC4 can be optionally configured to link against CLN, the Class
+Library for Numbers, available here:
 
   http://www.ginac.de/CLN/
 

diff --git a/GMP-LICENSE b/GMP-LICENSE
index 3903d111e366b76af513c20821ea9162a593fa01..bef2c0bf644173d28389ecd5132ae1fbfb39cee2 100644 (file)
--- a/GMP-LICENSE
+++ b/GMP-LICENSE
@@ -1,7 +1,12 @@
 --------------------------------------------------------------------------------
-CVC4 links against The GNU Multiple Precision Arithmetic Library, licensed
-under GNU LGPL v3. In the following we include a copy of the GNU GPL v3 license
-and the GNU LGPL v3 as required by GNU LGPL v3.
+CVC4 can be (and is by default) configured to link against The GNU Multiple
+Precision (GMP) Arithmetic Library, licensed under GNU's Lesser General Public
+License (LGPL), version 3.  Below, we include a copy of the GNU General Public
+License (GPL), version 3 followed by a copy of the GNU LGPL, version 3, as
+required by the LGPL.  Note that according to the terms of the LGPL, both
+CVC4's source, and the combined work (CVC4 linked with GMP) may (and do) remain
+under the more permissive CVC4 license (see the COPYING file included with
+CVC4's distribution).
 --------------------------------------------------------------------------------
 
                     GNU GENERAL PUBLIC LICENSE