Fix wording on GPL in legal notices; also remove an unnecessary source dependence.

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/COPYING b/COPYING
index 5c6be04c2e5f4f3b34a52ba92c977dc477023481..df32895e7394999aa9bf3676945dba6888207bd2 100644 (file)
--- a/COPYING
+++ b/COPYING
@@ -238,10 +238,10 @@ for Numbers, available here:
 
   http://www.ginac.de/CLN/
 
-Please be advised that as this class library is covered under the GPL, the
-combined work, CVC4+CLN, is also covered under the GPL and cannot be used
-by proprietary software projects.  For the full text of the GPL, please
-consult the CLN website.  CVC4 does not require CLN; it can be built against
-libgmp, the GNU Multiple Precision Arithmetic Library, which is covered by
-the more permissive LGPL.  To ensure that CLN is not used in the build,
-configure CVC4 with "--without-cln".
+Please be advised that as this class library is covered under the GPLv3, if
+you choose to use the combined work, "CVC4+CLN," by building CVC4 with CLN,
+then it is also covered under the GPLv3.  If you want to make sure you build
+a version of CVC4 that uses libgmp, the GNU Multiple Precision Arithmetic
+Library, configure CVC4 with "--with-gmp" before building (though that is the
+default).  It can then be used in contexts where you want to license CVC4
+under the (modified) BSD license.

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 8e61415e8722d6baaac55cc321402669ed6bbb4f..89e9ee316867deafb2831dc16da370bead678f71 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -39,7 +39,6 @@
 #include "expr/node_value.h"
 #include "context/context.h"
 #include "util/subrange_bound.h"
-#include "util/configuration_private.h"
 #include "util/tls.h"
 #include "options/options.h"
 

diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index b93a6dd5e3f3a137a2e1aac1d61242a629e7d5ca..dec982e32206ed67ea8d6a741fffc466f5936d55 100644 (file)
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -131,10 +131,10 @@ Copyright (C) 2009, 2010, 2011, 2012\n\
     ( IS_CLN_BUILD ? "\
 This CVC4 library uses CLN as its multi-precision arithmetic library.\n\n\
 CVC4 is open-source and is covered by the BSD license (modified).\n\
-However, CLN, the Class Library for Numbers, is covered by the GPL.  Thus\n\
-this CVC4 library cannot be used in proprietary applications.  Please\n\
-consult the CVC4 documentation for instructions about building a version\n\
-of CVC4 that links against GMP, and can be used in such applications.\n" : \
+However, CLN, the Class Library for Numbers, is covered by the GPLv3,\n\
+and so this \"combined\" work, CVC4+CLN, is covered by the GPLv3 as well\n\
+Please consult the CVC4 documentation for instructions about building\n\
+without CLN if you want to license CVC4 under the (modified) BSD license.\n" : \
 "This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\
 CVC4 is open-source and is covered by the BSD license (modified).\n\n\
 THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE IT AT YOUR OWN RISK.\n" ) )