summaryrefslogtreecommitdiff
path: root/COPYING
diff options
context:
space:
mode:
Diffstat (limited to 'COPYING')
-rw-r--r--COPYING19
1 files changed, 18 insertions, 1 deletions
diff --git a/COPYING b/COPYING
index 7008c8d90..02132ec28 100644
--- a/COPYING
+++ b/COPYING
@@ -2,7 +2,11 @@ CVC4 is copyright (C) 2009, 2010 the ACSys research group at the Courant
Institute for Mathematical Sciences, New York University.
All rights reserved.
-This is a prerelease version; distribution is restricted.
+CVC4 is open-source; distribution is under the terms of the modified BSD
+license. However, certain builds of CVC4 link against GPLed libraries,
+and therefore the use of these builds is restricted in non-open-source
+projects. See below for a discussion of CLN and how to ensure you have
+a build that doesn't link against GPLed libraries.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
''AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
@@ -115,3 +119,16 @@ Their copyright:
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+Certain builds of CVC4 link against a GPLed library, CLN, the Class Library
+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".
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback