Merge branch '1.3.x'

Conflicts:
	COPYING
	NEWS

10 files changed, 165 insertions, 123 deletions

diff --git a/COPYING b/COPYING
index dd6a1582a..4be4fdfa4 100644
--- a/COPYING
+++ b/COPYING
@@ -1,11 +1,15 @@
 CVC4 is copyright (C) 2009, 2010, 2011, 2012, 2013 New York University
 and The University of Iowa.  All rights reserved.
 
-CVC4 is open-source; distribution is under the terms of the modified BSD
-license.  However, certain builds of CVC4 link against GPLed libraries,
-and therefore the use of these builds is restricted in non-open-source
-projects.  See below for a discussion of CLN and GLPK, and how to ensure
-you have a build that doesn't link against GPLed libraries.
+The source code of CVC4 is open and available to students, researchers,
+software companies, and everyone else to study, to modify, and to
+redistribute original or modified versions; distribution is under the
+terms of the modified BSD license.  However, CVC4 can be configured (and
+is, by default) to link against some GPLed libraries, and therefore the
+use of these builds may be restricted in non-GPL-compatible projects.
+See below for a discussion of CLN, GLPK, and Readline (the three GPLed
+optional library dependences for CVC4), and how to ensure you have a
+build that doesn't link against GPLed libraries.
 
 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
 ''AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
@@ -19,7 +23,7 @@ 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.
 
--- Morgan Deters <mdeters@cs.nyu.edu>  Thu, 05 Dec 2013 14:22:26 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu>  Tue, 17 Dec 2013 14:35:55 -0500
 
 CVC4 incorporates MiniSat code, excluded from the above copyright.
 See src/sat/minisat.  Its copyright:
@@ -232,31 +236,41 @@ Their copyright:
   (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
   THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 
-Certain builds of CVC4 link against a GPLed library, CLN, the Class Library
-for Numbers, available here:
+CVC4 can be optionally configured to link against CLN, the Class Library for
+Numbers, available here:
 
   http://www.ginac.de/CLN/
 
 Please be advised that as this library is covered under the GPLv3, if you
 choose to use the combined work, "CVC4+CLN," by building CVC4 with CLN,
 then it is also covered under the GPLv3.  If you want to make sure you build
-a version of CVC4 that uses libgmp, the GNU Multiple Precision Arithmetic
-Library, configure CVC4 with "--with-gmp" 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.
+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.
 
-Certain builds of CVC4 link against a GPLed library, GLPK, the GNU Linear
+CVC4 can be optionally configured to link against GLPK, the GNU Linear
 Programming Kit, available here:
 
   http://www.gnu.org/software/glpk/
 
 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:
diff --git a/INSTALL b/INSTALL
index f0e1f6cc6..d8634f3e8 100644
--- a/INSTALL
+++ b/INSTALL
@@ -126,7 +126,12 @@ GLPK.
 The GNU Readline library is optionally used to provide command
 editing, tab completion, and history functionality at the CVC prompt
 (when running in interactive mode).  Check your distribution for a
-package named "libreadline-dev" or "readline-devel" or similar.
+package named "libreadline-dev" or "readline-devel" or similar.  This
+library is covered by the GNU General Public License, version 3.  Like
+the above-mentioned libraries, if you choose to use CVC4 with readline
+support, you are licensing CVC4 under that same license.  (Please visit
+http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html for more
+details about readline.)
 
 The Boost C++ threading library (often packaged independently of the
 Boost base library) is needed to run CVC4 in "portfolio"
diff --git a/NEWS b/NEWS
index 9f17bfaa4..dd1de35a4 100644
--- a/NEWS
+++ b/NEWS
@@ -5,6 +5,13 @@ Changes since 1.3
 
 * 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 --git a/README b/README
index c09fe979c..c5b751d0a 100644
--- a/README
+++ b/README
@@ -17,8 +17,8 @@ from any previous version.
 CVC4 is intended to be an open and extensible SMT engine.  It can be
 used as a stand-alone tool or as a library.  It has been designed to
 increase the performance and reduce the memory overhead of its
-predecessors.  It is written entirely in C++ and is released under a
-free software license (see the file COPYING in the source
+predecessors.  It is written entirely in C++ and is released under an
+open-source software license (see the file COPYING in the source
 distribution).
 
 *** Getting started with CVC4
diff --git a/config/cvc4.m4 b/config/cvc4.m4
index aefce193a..4b8b2e342 100644
--- a/config/cvc4.m4
+++ b/config/cvc4.m4
@@ -16,8 +16,9 @@ AC_DEFUN([CVC4_REWRITE_ARGS_FOR_BUILD_PROFILE],
 handle_option() {
   ac_option="$[]1"
   case $ac_option in
+    --bsd) ac_option='CVC4_BSD_LICENSED_CODE_ONLY=1' ;;
     -*|*=*) ;;
-    production|production-*|debug|debug-*|default|default-*|competition|competition-*)
+    production|production-*|debug|debug-*|competition|competition-*)
       # regexp `\?' not supported on Mac OS X
       ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'`
       ac_cvc4_build_profile_set=yes
diff --git a/config/readline.m4 b/config/readline.m4
index 44be9ff41..c298f3db4 100644
--- a/config/readline.m4
+++ b/config/readline.m4
@@ -9,6 +9,9 @@ readline_compentry_func_returns_charp=0
 READLINE_LIBS=
 if test "$with_readline" = no; then
   AC_MSG_RESULT([no, readline disabled by user])
+elif test "$with_readline" = check -a -n "$CVC4_BSD_LICENSED_CODE_ONLY"; then
+  AC_MSG_RESULT([no, user requested BSD-compatible dependences only])
+  with_readline=no
 else
   if test "$with_readline" = check; then
     AC_MSG_RESULT([no preference by user, will auto-detect])
diff --git a/configure.ac b/configure.ac
index 1cd7a4696..9650030c0 100644
--- a/configure.ac
+++ b/configure.ac
@@ -108,10 +108,10 @@ fi
 AC_MSG_CHECKING([for requested build profile])
 AC_ARG_WITH([build],
   [AS_HELP_STRING([--with-build=profile],
-     [for profile in {production,debug,default,competition,personal}])])
+     [for profile in {production,debug,competition,personal}])])
 
-if test -z "${with_build+set}" -o "$with_build" = default; then
-  with_build=default
+if test -z "${with_build+set}"; then
+  with_build=production
 fi
 if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}"; then
   custom_build_profile=no
@@ -238,11 +238,8 @@ AC_PROG_INSTALL
 
 CVC4_GCC_VERSION
 
-# [chris 8/24/2010] The user *must* specify --with-cln to get CLN
-# (and, thus, opt in to the GPL dependency).
-
-cvc4_use_gmp=0
-cvc4_use_cln=0
+cvc4_use_gmp=2
+cvc4_use_cln=2
 
 AC_ARG_WITH(
   [cln],
@@ -250,41 +247,49 @@ AC_ARG_WITH(
     [--with-cln],
     [use CLN instead of GMP]
   ),
-  [if test "$withval" != no; then
-     cvc4_use_cln=1
-   fi
+  [case "$withval" in
+   y|ye|yes|Y|YE|YES) cvc4_use_cln=1 ;;
+   n|no|N|NO) cvc4_use_cln=0 ;;
+   esac
   ]
 )
 
-# [chris 8/24/2010] --with-gmp has no practical effect, since GMP is
-# the default. Could be useful if other options are added later.
-
 AC_ARG_WITH(
   [gmp],
   AS_HELP_STRING(
     [--with-gmp],
-    [use GMP instead of CLN (default)]
+    [use GMP instead of CLN]
   ),
-  [if test "$withval" = no; then
-     if test $cvc4_use_cln = 0; then
-       AC_MSG_ERROR([You must use either CLN and GMP.  Please pick one.])
-     fi
-   else
-     cvc4_use_gmp=1
-   fi
+  [case "$withval" in
+   y|ye|yes|Y|YE|YES) cvc4_use_gmp=1 ;;
+   n|no|N|NO) cvc4_use_gmp=0 ;;
+   esac
   ]
 )
 
-if test $cvc4_use_cln = 1 && test $cvc4_use_gmp = 1; then
-  # error
-  AC_MSG_ERROR([You cannot use both CLN and GMP.  Please pick one.])
+if test $cvc4_use_cln = 1 -a $cvc4_use_gmp = 1 || test $cvc4_use_cln = 0 -a $cvc4_use_gmp = 0; then
+  AC_MSG_ERROR([You must use either CLN and GMP.  Please pick one.])
+fi
+if test $cvc4_use_gmp = 1; then
+  cvc4_use_cln=0
+elif test $cvc4_use_gmp = 0; then
+  cvc4_use_cln=1
+elif test $cvc4_use_cln = 1; then
+  cvc4_use_gmp=0
+elif test $cvc4_use_cln = 0; then
+  cvc4_use_gmp=1
 fi
 
 # try GMP, fail if not found; GMP is required for both CLN and for GMP
 # versions of CVC4
 AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
 
-if test $cvc4_use_cln = 1; then
+if test $cvc4_use_cln = 2 -a -n "$CVC4_BSD_LICENSED_CODE_ONLY"; then
+  cvc4_use_cln=0
+  cvc4_use_gmp=1
+fi
+
+if test $cvc4_use_cln != 0; then
   # [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
   # gracefully.  You can only specify it once for a given library name.  That
   # is, even on separate if/else branches, you can't put
@@ -296,12 +301,12 @@ if test $cvc4_use_cln = 1; then
      AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])])
      AC_LANG_POP([C++])
     ],
-    [if test $cvc4_use_cln = 0; then
-       # fall back to GMP
-       AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
-     else
+    [if test $cvc4_use_cln = 1; then
        # fail
        AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
+     else
+       # fall back to GMP
+       AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
      fi
     ]
   )
@@ -332,11 +337,6 @@ if test -z "$ac_confdir"; then
   ac_confdir="$srcdir"
 fi
 build_type=`$ac_confdir/config/build-type $with_build $btargs $cvc4_cln_or_gmp`
-if test "$custom_build_profile" = yes; then
-  if test "$with_build" = default; then
-    build_type=`$ac_confdir/config/build-type custom $btargs $cvc4_cln_or_gmp`
-  fi
-fi
 AC_MSG_RESULT($build_type)
 
 # Require building in target and build-specific build directory:
@@ -899,7 +899,7 @@ if test -z "$LFSC"; then
 elif test "$enable_proof" = yes; then
   support_proof_tests='yes, proof regression tests enabled'
 else
-  support_proof_tests='no, proof generation disabled for this build'
+  support_proof_tests='no, proof-generation disabled for this build'
 fi
 AC_SUBST([LFSC])
 AC_SUBST([LFSCARGS])
@@ -1290,29 +1290,12 @@ fi
 
 AM_CONDITIONAL([CVC4_NEEDS_REPLACEMENT_FUNCTIONS], [test -n "$LIBOBJS"])
 
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
-
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
-CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
-
-AC_OUTPUT
-
 # Final information to the user
+gpl=no
 licensewarn=
 
 if test "$custom_build_profile" = yes; then
-  if test "$with_build" = default; then
-    with_build=custom
-  else
-    with_build="$with_build (customized)"
-  fi
+  with_build="$with_build (customized)"
 fi
 
 support_unit_tests='cxxtest not found; unit tests not supported'
@@ -1329,46 +1312,50 @@ else
 fi
 
 if test $have_libglpk -eq 1; then
-  licensewarn="${licensewarn}Please note that CVC4 will be built against the GNU Linear Programming
-Kit (GLPK).  This library is covered under the GPL, so use of this build
-of CVC4 will be more restrictive than CVC4's license would normally
-suggest.  For full details of GLPK and its license, please visit
-  http://www.gnu.org/software/glpk/
-To build CVC4 without GLPK, configure --without-glpk (which is the default).
+  gpl=yes
+  gpllibs="${gpllibs} glpk"
+fi
 
-"
+if test $have_libreadline -eq 1; then
+  gpl=yes
+  gpllibs="${gpllibs} readline"
 fi
 
 if test $cvc4_cln_or_gmp = cln; then
   mplibrary='cln (GPL)'
-  licensewarn="${licensewarn}Please note that CVC4 will be built against the Class Library for
-Numbers (CLN).  This library is covered under the GPL, so use of this
-build of CVC4 will be more restrictive than CVC4's license would
-normally suggest.  For full details of CLN and its license, please visit
-  http://www.ginac.de/CLN/
-To build CVC4 with GMP instead (which is covered under the more permissive
-LGPL), configure --without-cln.
-
-"
+  gpl=yes
+  gpllibs="${gpllibs} cln"
   if test $with_portfolio = yes; then
-    licensewarn="${licensewarn}
-WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
-WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
-
-Note that CLN is UNSAFE FOR USE in parallel contexts!
-This build of CVC4 cannot be used safely as a portfolio solver.
-since the result of building with CLN will include numerous race
-conditions on the refcounts internal to CLN.
-
-WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
-WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING * WARNING
+    AC_ERROR([Bad configuration detected: cannot build portfolio with CLN.
+Please specify only one of --with-portfolio and --with-cln.])
+  fi
+else
+  mplibrary='gmp'
+fi
 
-"
+if test "$gpl" = yes; then
+  if test -n "$CVC4_BSD_LICENSED_CODE_ONLY"; then
+    AC_ERROR([Bad configuration detected: user requested BSD-licensed code only, but also requested GPLed libraries:$gpllibs])
   fi
+
+  licensewarn="${licensewarn}"'****************************************************************************
+Please note that CVC4 will be built against the following GPLed libraries:
+ '"$gpllibs"'
+As these libraries are covered under the GPLv3, so is this build of CVC4.
+CVC4 is also available to you under the terms of the (modified) BSD license.
+If you prefer to license CVC4 under those terms, please configure with the
+option "--bsd".
+****************************************************************************
+
+'
+  license="GPLv3 (due to optional libraries; see below)"
 else
-  mplibrary='gmp (LGPL)'
+  license="modified BSD"
 fi
 
+if test "$gpl" = yes; then isgpl=1; else isgpl=0; fi
+AC_DEFINE_UNQUOTED(CVC4_GPL_DEPS, $isgpl, [Whether CVC4 is built with the (optional) GPLed library dependences.])
+
 CVC4_COMPAT_LIBRARY_VERSION_or_nobuild="$CVC4_COMPAT_LIBRARY_VERSION"
 CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="$CVC4_BINDINGS_LIBRARY_VERSION"
 if test "$CVC4_BUILD_LIBCOMPAT" = no; then
@@ -1386,6 +1373,20 @@ if test -n "$CVC4_LANGUAGE_BINDINGS"; then
   fi
 fi
 
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/integer.h])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h])
+
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3])
+CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3])
+
+AC_OUTPUT
+
 cat <<EOF
 
 CVC4 $VERSION
@@ -1394,7 +1395,7 @@ Build profile: $with_build
 Build ID     : $build_type
 Optimized    : $optimized
 Debug symbols: $enable_debug_symbols
-Proof        : $enable_proof
+Proofs       : $enable_proof
 Statistics   : $enable_statistics
 Replay       : $enable_replay
 Assertions   : $enable_assertions
@@ -1406,7 +1407,6 @@ Unit tests   : $support_unit_tests
 Proof tests  : $support_proof_tests
 gcov support : $enable_coverage
 gprof support: $enable_profiling
-Readline     : $with_readline
 
 Static libs  : $enable_static
 Shared libs  : $enable_shared
@@ -1420,6 +1420,7 @@ Portfolio    : $with_portfolio
 
 MP library   : $mplibrary
 GLPK         : $with_glpk
+Readline     : $with_readline
 
 CPPFLAGS     : $CPPFLAGS
 CXXFLAGS     : $CXXFLAGS
@@ -1434,6 +1435,8 @@ libcvc4bindings version: $CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild
 
 Install into : $prefix
 
+CVC4 license : $license
+
 ${licensewarn}Now just type make, followed by make check or make install, as you like.
 
 EOF
diff --git a/src/main/options b/src/main/options
index ba36e43ab..faac6b8f1 100644
--- a/src/main/options
+++ b/src/main/options
@@ -7,6 +7,7 @@ module DRIVER "main/options.h" Driver
 
 common-option version -V --version/ bool
  identify this CVC4 binary
+alias --license = --version
 
 common-option help -h --help/ bool
  full command line reference
diff --git a/src/util/configuration.h b/src/util/configuration.h
index be49e3dcf..696b67715 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -83,12 +83,16 @@ public:
 
   static std::string about();
 
+  static bool licenseIsGpl();
+
   static bool isBuiltWithGmp();
 
   static bool isBuiltWithCln();
 
   static bool isBuiltWithGlpk();
 
+  static bool isBuiltWithReadline();
+
   static bool isBuiltWithCudd();
 
   static bool isBuiltWithTlsSupport();
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index e33c5fa36..5d078b5ef 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -107,6 +107,18 @@ namespace CVC4 {
 #  define IS_GLPK_BUILD false
 #endif /* CVC4_USE_GLPK */
 
+#ifdef HAVE_LIBREADLINE
+#  define IS_READLINE_BUILD true
+#else /* HAVE_LIBREADLINE */
+#  define IS_READLINE_BUILD false
+#endif /* HAVE_LIBREADLINE */
+
+#if CVC4_GPL_DEPS
+#  define IS_GPL_BUILD true
+#else /* CVC4_GPL_DEPS */
+#  define IS_GPL_BUILD false
+#endif /* CVC4_GPL_DEPS */
+
 #ifdef TLS
 #  define USING_TLS true
 #else /* TLS */
@@ -126,24 +138,16 @@ compiled with " + ::CVC4::Configuration::getCompiler() + "\n\
 on " + ::CVC4::Configuration::getCompiledDateTime() + "\n\n\
 Copyright (C) 2009, 2010, 2011, 2012, 2013\n\
   New York University and The University of Iowa\n\n" + \
-    ( IS_CLN_BUILD ? "\
-This CVC4 library uses CLN as its multi-precision arithmetic library.\n\n\
-CVC4 is open-source and is covered by the BSD license (modified).\n\
-However, CLN, the Class Library for Numbers, is covered by the GPLv3,\n\
-and so this \"combined\" work, CVC4+CLN, is covered by the GPLv3 as well.\n\
-Please consult the CVC4 documentation for instructions about building\n\
-without CLN if you want to license CVC4 under the (modified) BSD license.\n\n\
-" : ( IS_GLPK_BUILD ? "\
-This CVC4 library uses GLPK in its arithmetic solver.\n\n\
-CVC4 is open-source and is covered by the BSD license (modified).\n\
-However, GLPK, the GNU Linear Programming Kit, is covered by the GPLv3,\n\
-and so this \"combined\" work, CVC4+GLPK, is covered by the GPLv3 as well.\n\
-Please consult the CVC4 documentation for instructions about building\n\
-without GLPK if you want to license CVC4 under the (modified) BSD license.\n\n\
+    ( IS_GPL_BUILD ? "\
+This build of CVC4 uses GPLed libraries, and is thus covered by the GNU\n\
+General Public License (GPL) version 3.  Versions of CVC4 are available\n\
+that are covered by the (modified) BSD license.  If you want to license\n\
+CVC4 under this license, please configure CVC4 with the \"--bsd\" option\n\
+before building from sources.\n\
 " : \
 "This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\
 CVC4 is open-source and is covered by the BSD license (modified).\n\n\
-" ) ) + "\
+" ) + "\
 THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE AT YOUR OWN RISK.\n\n\
 See the file COPYING (distributed with the source code, and with all binaries)\n\
 for the full CVC4 copyright, licensing, and (lack of) warranty information.\n" )