summaryrefslogtreecommitdiff
path: root/COPYING
diff options
context:
space:
mode:
Diffstat (limited to 'COPYING')
-rw-r--r--COPYING21
1 files changed, 21 insertions, 0 deletions
diff --git a/COPYING b/COPYING
index c02b10910..4bccb1d13 100644
--- a/COPYING
+++ b/COPYING
@@ -272,3 +272,24 @@ you build a version of CVC4 that uses no GPLed libraries, configure CVC4 with
the "--bsd" option before building (which is the default). CVC4 can then be
used in contexts where you want to license CVC4 under the (modified) BSD
license.
+
+CVC4 sources incorporate those of the LFSC proof checker, which is
+covered by the following license:
+
+ LFSC is copyright (C) 2012, 2013 The University of Iowa. All rights
+ reserved.
+
+ LFSC is open-source; distribution is under the terms of the modified
+ BSD license.
+
+ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
+ AS IS AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ 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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback