diff options
| -rw-r--r-- | COPYING | 15 | ||||
| -rw-r--r-- | GMP-LICENSE | 11 |
2 files changed, 17 insertions, 9 deletions
@@ -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 3903d111e..bef2c0bf6 100644 --- 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 |