Handle Z3 API change between 4.4.1 and the current master branch

for the ``Z3_get_error_msg()`` function.

4 files changed, 60 insertions, 1 deletions

diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 94928fcc..617469e6 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -651,6 +651,22 @@ if test "X$ENABLE_Z3" != X0 ; then
            AC_MSG_ERROR([Unable to link against z3])
     ], "$Z3_LDFLAGS")
 
+    # Test which function signature of ``Z3_get_error_msg()`` we need to use.
+    # There's an API break between Z3 4.4.1 and the master branch
+    AC_MSG_CHECKING([if Z3_get_error_msg() requires Z3_context])
+    AC_COMPILE_IFELSE(
+      [AC_LANG_PROGRAM([[#include "z3.h"]],
+                       [[Z3_context c = Z3_mk_context(0); Z3_get_error_msg(c, Z3_OK);]])],
+      [Z3_HAS_ERROR_MSG_CONTEXT=1],
+      [Z3_HAS_ERROR_MSG_CONTEXT=0])
+
+    if test "X$Z3_HAS_ERROR_MSG_CONTEXT" == X1; then
+      AC_DEFINE(HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT, [1], [Z3 needs a Z3_context passed to Z3_get_error_msg()])
+      AC_MSG_RESULT([yes])
+    else
+      AC_MSG_RESULT([no])
+    fi
+
     Z3_LDFLAGS="${Z3_LDFLAGS} -lz3"
     AC_MSG_NOTICE([Using Z3 solver backend])
     CPPFLAGS="$old_CPPFLAGS"
diff --git a/configure b/configure
index 571c4338..4da72718 100755
--- a/configure
+++ b/configure
@@ -5109,6 +5109,39 @@ else
 fi
 
 
+    # Test which function signature of ``Z3_get_error_msg()`` we need to use.
+    # There's an API break between Z3 4.4.1 and the master branch
+    { $as_echo "$as_me:${as_lineno-$LINENO}: checking if Z3_get_error_msg() requires Z3_context" >&5
+$as_echo_n "checking if Z3_get_error_msg() requires Z3_context... " >&6; }
+    cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+#include "z3.h"
+int
+main ()
+{
+Z3_context c = Z3_mk_context(0); Z3_get_error_msg(c, Z3_OK);
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_cxx_try_compile "$LINENO"; then :
+  Z3_HAS_ERROR_MSG_CONTEXT=1
+else
+  Z3_HAS_ERROR_MSG_CONTEXT=0
+fi
+rm -f core conftest.err conftest.$ac_objext conftest.$ac_ext
+
+    if test "X$Z3_HAS_ERROR_MSG_CONTEXT" == X1; then
+
+$as_echo "#define HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT 1" >>confdefs.h
+
+      { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
+$as_echo "yes" >&6; }
+    else
+      { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+    fi
+
     Z3_LDFLAGS="${Z3_LDFLAGS} -lz3"
     { $as_echo "$as_me:${as_lineno-$LINENO}: Using Z3 solver backend" >&5
 $as_echo "$as_me: Using Z3 solver backend" >&6;}
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 28eefcb6..66bf31cb 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -63,6 +63,9 @@
 /* Define to 1 if you have the <unistd.h> header file. */
 #undef HAVE_UNISTD_H
 
+/* Z3 needs a Z3_context passed to Z3_get_error_msg() */
+#undef HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT
+
 /* LLVM version is release (instead of development) */
 #undef LLVM_IS_RELEASE
 
diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp
index f928c927..ae78c21c 100644
--- a/lib/Solver/Z3Builder.cpp
+++ b/lib/Solver/Z3Builder.cpp
@@ -27,7 +27,14 @@ llvm::cl::opt<bool> UseConstructHashZ3(
 }
 
 void custom_z3_error_handler(Z3_context ctx, Z3_error_code ec) {
-  ::Z3_string errorMsg = Z3_get_error_msg(ctx, ec);
+  ::Z3_string errorMsg =
+#ifdef HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT
+      // Z3 > 4.4.1
+      Z3_get_error_msg(ctx, ec);
+#else
+      // Z3 4.4.1
+      Z3_get_error_msg(ec);
+#endif
   // FIXME: This is kind of a hack. The value comes from the enum
   // Z3_CANCELED_MSG but this isn't currently exposed by Z3's C API
   if (strcmp(errorMsg, "canceled") == 0) {