Merge branch '1.3.x'

Conflicts:
	COPYING
	NEWS

diff --cc COPYING
index dd6a1582a4e04ff975acf725f3c4975f580640e0,8babef432f97545d8ec63907a841d5b461df0d4b..4be4fdfa48bfb0af9d5f5e5fda41ef64b9352634
--- 1/COPYING
--- 2/COPYING
+++ b/COPYING
@@@ -252,29 -255,19 +255,40 @@@ Programming Kit, available here
  
  Please be advised that as this library is covered under the GPLv3, if
  you choose to use the combined work, "CVC4+GLPK," by building CVC4 with
- GLPK, then it is also covered under the GPLv3.  If you want to make sure
- 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.
+ GLPK, then it is also covered under the GPLv3.  If you want to make sure you
+ build a version of CVC4 that uses no GPLed libraries, configure CVC4 with the
+ "--bsd" option before building.  CVC4 can then be used in contexts where you
+ want to license CVC4 under the (modified) BSD license.
+ 
+ CVC4 can be optionally configured to link against GNU Readline for improved
+ text-editing support in interactive mode.  GNU Readline is available here:
+ 
+   http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html
+ 
+ Please be advised that as this library is covered under the GPLv3, if
+ you choose to use the combined work, "CVC4+Readline," by building CVC4 with
+ Readline, then it is also covered under the GPLv3.  If you want to make sure
+ you build a version of CVC4 that uses no GPLed libraries, configure CVC4 with
+ the "--bsd" option before building.  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.

diff --cc NEWS
index 9f17bfaa4622ba19d56fa03e7b3edd6818ba4097,5c42481b414760699fffe2751d16879ed484d7da..dd1de35a454ef58f118d88bd31ed442fecbfc931
--- 1/NEWS
--- 2/NEWS
+++ b/NEWS
@@@ -4,7 -4,13 +4,14 @@@ Changes since 1.
  =================
  
  * Timed statistics are now properly updated even on process abort.
 +* The LFSC proof checker has been incorporated into CVC4 sources.
+ * By default, CVC4 builds in "production" mode (optimized, with fewer
+   internal checks on).  The common alternative is a "debug" build, which
+   is much slower.  CVC4 also builds with GPL dependences by default now
+   (if those libraries are available), as this is the best-performing
+   version of CVC4.  However, the new configure option "--bsd" disables
+   these GPL dependences and builds the best-performing BSD-licenced version
+   of CVC4.
  
  Changes since 1.2
  =================

diff --cc configure.ac
Simple merge