summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTianyi Liang <tianyi-liang@uiowa.edu>2013-12-19 12:01:28 -0600
committerTianyi Liang <tianyi-liang@uiowa.edu>2013-12-19 12:01:28 -0600
commit2149ccfe0ab56bcd2661f506e8b7d1ee72896ba3 (patch)
treebf57bd57e84b71122c4a748d228125126a3f40fd
parent49b8468cfd4921cdc939a1483bbf028f55951744 (diff)
parentc33d53d005c41cf5705a85f86311d8d0142d2a01 (diff)
Merge branch 'master' of https://github.com/CVC4/CVC4
-rw-r--r--configure.ac26
-rw-r--r--proofs/lfsc_checker/configure.ac2
-rw-r--r--test/Makefile.am1
3 files changed, 23 insertions, 6 deletions
diff --git a/configure.ac b/configure.ac
index 763148d73..38f5681fc 100644
--- a/configure.ac
+++ b/configure.ac
@@ -10,7 +10,7 @@ m4_define(_CVC4_RELEASE_STRING, _CVC4_MAJOR[.]_CVC4_MINOR[]m4_if(_CVC4_RELEASE,[
dnl Preprocess CL args. Defined in config/cvc4.m4
CVC4_AC_INIT
-AC_PREREQ([2.68])
+AC_PREREQ([2.61])
AC_INIT([cvc4], _CVC4_RELEASE_STRING, [cvc-bugs@cs.nyu.edu])
AC_CONFIG_SRCDIR([src/include/cvc4_public.h])
AC_CONFIG_AUX_DIR([config])
@@ -298,9 +298,23 @@ if test $cvc4_use_cln != 0; then
# PKG_CHECK_MODULES([CLN], ...). That's why things are so convoluted here,
# we have to have PKG_CHECK_MODULES _exactly_ once in configure.ac !
PKG_CHECK_MODULES([CLN], [cln >= 1.2.2],
- [cvc4_use_cln=1
- AC_LANG_PUSH([C++])
- AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])])
+ [AC_LANG_PUSH([C++])
+ save_LIBS="$LIBS"
+ LIBS="$CLN_LIBS $LIBS"
+ AC_LINK_IFELSE([AC_LANG_PROGRAM([[#include <cln/cln.h>]], [[cln::cl_F pi = "3.1415926";]])], [
+ cvc4_use_cln=1
+ ], [
+ if test $cvc4_use_cln = 1; then
+ # fail
+ AC_MSG_ERROR([CLN installation missing, too old, or not functional for this architecture])
+ else
+ # fall back to GMP
+ AC_MSG_NOTICE([CLN installation missing, too old, or not functional for this architecture, will use gmp instead])
+ cvc4_use_cln=0
+ cvc4_use_gmp=1
+ fi
+ ])
+ LIBS="$save_LIBS"
AC_LANG_POP([C++])
],
[if test $cvc4_use_cln = 1; then
@@ -309,6 +323,8 @@ if test $cvc4_use_cln != 0; then
else
# fall back to GMP
AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
+ cvc4_use_cln=0
+ cvc4_use_gmp=1
fi
]
)
@@ -1346,7 +1362,7 @@ Please note that CVC4 will be built against the following GPLed libraries:
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".
+option "--bsd", which will disable all optional GPLed library dependences.
****************************************************************************
'
diff --git a/proofs/lfsc_checker/configure.ac b/proofs/lfsc_checker/configure.ac
index 245b0ea65..5f4353664 100644
--- a/proofs/lfsc_checker/configure.ac
+++ b/proofs/lfsc_checker/configure.ac
@@ -1,7 +1,7 @@
# -*- Autoconf -*-
# Process this file with autoconf to produce a configure script.
-AC_PREREQ([2.68])
+AC_PREREQ([2.61])
AC_INIT([lfsc-checker], [1.0], [cvc-bugs@cs.nyu.edu])
AC_CONFIG_SRCDIR([libwriter.h])
AC_CONFIG_AUX_DIR([config])
diff --git a/test/Makefile.am b/test/Makefile.am
index 104d40ab1..8a7a5a0a7 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -57,6 +57,7 @@ subdirs_to_check = \
regress/regress0/fmf \
regress/regress0/strings \
regress/regress1 \
+ regress/regress1/arith \
regress/regress2 \
regress/regress3
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback