Using clang-2.9 with Os X 10.5.8 for compiling Z3

Question

I would like to use Z3Py and I am trying to install Z3 following the instructions in http://z3.codeplex.com/SourceControl/changeset/view/89c1785b7322#README I am obtaining the following:

dhcp-154:z3-89c1785b7322 mgarcia$ ./configure CXX=clang++
checking whether we are using the GNU C++ compiler... no
checking whether clang++ accepts -g... no
checking for gcc... gcc
checking whether we are using the GNU C compiler... no
checking whether gcc accepts -g... no
checking for gcc option to accept ISO C89... unsupported
checking whether make sets $(MAKE)... yes
checking for grep that handles long lines and -e... /usr/bin/grep
checking for a sed that does not truncate output... /usr/bin/sed
checking for int *... no
checking size of int *... 4
configure: creating ./config.status
config.status: creating scripts/config-debug.mk
config.status: creating scripts/config-release.mk
Z3 was configured with success.
Host platform:  osx
Compiler:       clang++
Arithmetic:     internal
Python:         python
Prefix:         /usr
64-bit:         no

and when I do the make I get errors as for instance:

In file included from ../src/muz_qe/dl_smt_relation.cpp:32:
../src/smt/expr_context_simplifier.h:78:10: error: expected parameter declarator
    void assert(expr* e) { m_solver.assert_expr(e); }

/usr/include/assert.h:85:23: note: instantiated from:
    (__builtin_expect(!(e), 0) ? __assert_rtn(__func__, __FILE__, __LINE__, #e) : (void)0)

In file included from ../src/muz_qe/dl_smt_relation.cpp:32:
../src/smt/expr_context_simplifier.h:78:10: error: expected ')'
../src/smt/expr_context_simplifier.h:78:10: note: to match this '('
    void assert(expr* e) { m_solver.assert_expr(e); }

So I do not know if this is a problem related with the code or I am still missing something. Or, maybe, I am using really older versions.

Thank you for your answers.

Answer 1

I don't have a similar system here to test, but I believe this is because your system library uses something like

#define assert(x) (__builtin_expect...

to define the assert function. It happens that one of the functions in one of our classes was called assert as well and the preprocessor replaces that with the rest of the #define. It seems that this problem is already fixed in the unstable branch of Z3, which you can get from the source code download on Codeplex, by switching the branch selector from "master" to "unstable" before clicking on Download.