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 40cbdaa6b..dd6a1582a 100644
--- a/COPYING
+++ b/COPYING
@@ -257,3 +257,24 @@ you build a version of CVC4 that does not use GLPK, configure CVC4 with
"--without-glpk" 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.
+
+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