Merge branch '1.3.x'

Conflicts:
	COPYING
	NEWS
	config/cvc4.m4

diff --cc .travis.yml
Simple merge

diff --cc COPYING
index 28e814415ea4afe873a09bbf3f07590075d09faf,c02b10910103ce11102d0df4caf1dbc8e6e0235f..4bccb1d13990ec911109009fccb92de1289b6e3c
--- 1/COPYING
--- 2/COPYING
+++ b/COPYING
@@@ -269,26 -269,6 +269,27 @@@ Please be advised that as this library 
  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.
+ 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.

diff --cc NEWS
index d30c0ab778ce680988e1e7f67dde2c8f5239637f,05234ebff87d9cddefdc0ffc32ca73a3d4f933af..f0159f4a14f04b94cc4efb209e78f7c8b437f1d9
--- 1/NEWS
--- 2/NEWS
+++ b/NEWS
@@@ -4,16 -4,13 +4,16 @@@ 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.
+   is much slower.  By default, CVC4 builds with no GPL'ed dependences.
+   However, this is not the best-performing version; for that, you should
+   configure with "--enable-gpl --best", which links against GPL'ed
+   libraries that improve usability and performance.  For details on
+   licensing and dependences, see the README file.
 +* Small API adjustments to Datatypes to even out the API and make it
 +  function better in Java.
  * Better automatic handling of output language setting when using CVC4
    via API.  Previously, the "automatic" language setting was sometimes
    (though not always) defaulting to the internal "AST" language; it

diff --cc config/cvc4.m4
index 87d984ab4851e7258516b0a130fb43fec66da45c,7c2f6c82d68cf4c77f4c56083eff3400cb033a91..40e2054e6264c46f710b6d6e73cc27176fad0c3f
--- 1/config/cvc4.m4
--- 2/config/cvc4.m4
+++ b/config/cvc4.m4
@@@ -16,9 -24,26 +24,29 @@@ Licensing and performance options
  handle_option() {
    ac_option="$[]1"
    case $ac_option in
-     --bsd) ac_option='CVC4_BSD_LICENSED_CODE_ONLY=1' ;;
-     -enable-proofs | --enable-proofs) ac_option='--enable-proof' ;;
-     -*|*=*) ;;
+     --bsd|--disable-gpl|CVC4_BSD_LICENSED_CODE_ONLY=1)
+       if test "$CVC4_LICENSE_OPTION" = gpl; then AC_ERROR([cannot give both --bsd and --enable-gpl]); fi
+       CVC4_LICENSE_OPTION=bsd
+       ac_option="CVC4_BSD_LICENSED_CODE_ONLY=1"
+       eval $ac_option
+       ;;
+     --enable-gpl|--gpl|CVC4_BSD_LICENSED_CODE_ONLY=0)
+       if test "$CVC4_LICENSE_OPTION" = bsd; then AC_ERROR([cannot give both --bsd and --enable-gpl]); fi
+       CVC4_LICENSE_OPTION=gpl
+       ac_option="CVC4_BSD_LICENSED_CODE_ONLY=0"
+       eval $ac_option
+       ;;
+     --best)
+       # set the best configuration
+       handle_option --with-readline
+       handle_option --with-cln
+       return
+       ;;
++    -enable-proofs|--enable-proofs)
++      ac_option='--enable-proof'
++      ;;
+     -*|*=*)
+       ;;
      production|production-*|debug|debug-*|competition|competition-*)
        # regexp `\?' not supported on Mac OS X
        ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'`

diff --cc configure.ac
Simple merge