Fix two issues with AC_LINK_IFELSE for metaSMT:

1. It expects only 2 arguments, so if linking succeeds, nothing will happen (thanks to []),
otherwise the message "checking for new_bitvector() in -lmetaSMT" will appear.
The latter is that what we currently observe, which means linking actually failed.

2. The reason for linking failure is the use of "-lmetaSMT" in LDFLAGS.
AC_LINK_IFELSE does approximately the following: ${CXX} ... -lmetaSMT ${EXECUTABLE_NAME} ${LIBS},
which causes "libmetaSMT cannot be found" (at least on Ubuntu Xenial, where ${LIBS} = -lz).
After consulting https://www.gnu.org/software/autoconf/manual/autoconf-2.66/html_node/Running-the-Linker.html,
adding "-lmetaSMT" to ${LIBS} seems to be the correct solution.

2 files changed, 23 insertions, 8 deletions

diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 4da750cb..e732ffc4 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -803,16 +803,23 @@ else
   dnl AC_LANG(C++)
   old_CPPFLAGS="$CPPFLAGS"
   old_LDFLAGS="$LDFLAGS"
+  old_LIBS="$LIBS"
   CPPFLAGS="$CPPFLAGS -I$metasmt_root/include"
-  LDFLAGS="$LDFLAGS -L$metasmt_root/lib -lmetaSMT"
+  LDFLAGS="$LDFLAGS -L$metasmt_root/lib"
+  LIBS="$LIBS -lmetaSMT"
+
   AC_CHECK_HEADERS([$metasmt_root/include/metaSMT/DirectSolver_Context.hpp $metasmt_root/include/metaSMT/frontend/QF_BV.hpp],, [
          AC_MSG_ERROR([Unable to use $metasmt_root/include/metaSMT/DirectSolver_Context.hpp header])
   ])
+  AC_MSG_CHECKING([for new_bitvector() in -lmetaSMT])
   AC_LINK_IFELSE(
-      [AC_LANG_PROGRAM([#include $metasmt_root/include/metaSMT/frontend/QF_BV.hpp], [metaSMT::logic::QF_BV::new_bitvector(3)])],
-      [],[AC_MSG_CHECKING([for new_bitvector() in -lmetaSMT])],[AC_MSG_ERROR([Unable to link with libmetaSMT])])
+      [AC_LANG_PROGRAM([#include <metaSMT/frontend/QF_BV.hpp>], [metaSMT::logic::QF_BV::new_bitvector(3)])],
+            [AC_MSG_RESULT([yes])],
+            [AC_MSG_RESULT([no])
+             AC_MSG_ERROR([Unable to link with libmetaSMT])])
   CPPFLAGS="$old_CPPFLAGS"
   LDFLAGS="$old_LDFLAGS"
+  LIBS="$old_LIBS"
 
   AC_DEFINE(ENABLE_METASMT, 1, [Enable metaSMT API])
   AC_SUBST(METASMT_ROOT,$metasmt_root)
diff --git a/configure b/configure
index 5d8386ac..6f462669 100755
--- a/configure
+++ b/configure
@@ -5481,8 +5481,11 @@ else
 
     old_CPPFLAGS="$CPPFLAGS"
   old_LDFLAGS="$LDFLAGS"
+  old_LIBS="$LIBS"
   CPPFLAGS="$CPPFLAGS -I$metasmt_root/include"
-  LDFLAGS="$LDFLAGS -L$metasmt_root/lib -lmetaSMT"
+  LDFLAGS="$LDFLAGS -L$metasmt_root/lib"
+  LIBS="$LIBS -lmetaSMT"
+
   for ac_header in $metasmt_root/include/metaSMT/DirectSolver_Context.hpp $metasmt_root/include/metaSMT/frontend/QF_BV.hpp
 do :
   as_ac_Header=`$as_echo "ac_cv_header_$ac_header" | $as_tr_sh`
@@ -5500,9 +5503,11 @@ fi
 
 done
 
+  { $as_echo "$as_me:${as_lineno-$LINENO}: checking for new_bitvector() in -lmetaSMT" >&5
+$as_echo_n "checking for new_bitvector() in -lmetaSMT... " >&6; }
   cat confdefs.h - <<_ACEOF >conftest.$ac_ext
 /* end confdefs.h.  */
-#include $metasmt_root/include/metaSMT/frontend/QF_BV.hpp
+#include <metaSMT/frontend/QF_BV.hpp>
 int
 main ()
 {
@@ -5512,15 +5517,18 @@ metaSMT::logic::QF_BV::new_bitvector(3)
 }
 _ACEOF
 if ac_fn_cxx_try_link "$LINENO"; then :
-
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
+$as_echo "yes" >&6; }
 else
-  { $as_echo "$as_me:${as_lineno-$LINENO}: checking for new_bitvector() in -lmetaSMT" >&5
-$as_echo_n "checking for new_bitvector() in -lmetaSMT... " >&6; }
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+             as_fn_error $? "Unable to link with libmetaSMT" "$LINENO" 5
 fi
 rm -f core conftest.err conftest.$ac_objext \
     conftest$ac_exeext conftest.$ac_ext
   CPPFLAGS="$old_CPPFLAGS"
   LDFLAGS="$old_LDFLAGS"
+  LIBS="$old_LIBS"
 
 
 $as_echo "#define ENABLE_METASMT 1" >>confdefs.h