First attempt at incorporating LFSC proof checker into CVC4.

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.