Error when compiling a Haskell program using the Z3 library

[ghost]

Hi,

I'm using Z3 4.7.1, and when compiling the Haskell program which using the Z3 library (https://github.com/IagoAbal/haskell-z3), I encountered the following errors:

ghc z3.hs
Linking z3 ...
/home/trungtq/.cabal/lib/x86_64-linux-ghc-8.0.2/z3-4.3.1-BQQcEJY5Khr2mxtgsr1pQ9/libHSz3-4.3.1-BQQcEJY5Khr2mxtgsr1pQ9.a(Base.o):(.text+0x1595a): referencia a `Z3_get_parser_error' sin definir
/home/trungtq/.cabal/lib/x86_64-linux-ghc-8.0.2/z3-4.3.1-BQQcEJY5Khr2mxtgsr1pQ9/libHSz3-4.3.1-BQQcEJY5Khr2mxtgsr1pQ9.a(C.o):(.text+0xd7bc): referencia a `Z3_add_func_interp' sin definir
/home/trungtq/.cabal/lib/x86_64-linux-ghc-8.0.2/z3-4.3.1-BQQcEJY5Khr2mxtgsr1pQ9/libHSz3-4.3.1-BQQcEJY5Khr2mxtgsr1pQ9.a(C.o):(.text+0xd93f): referencia a `Z3_add_const_interp' sin definir
/home/trungtq/.cabal/lib/x86_64-linux-ghc-8.0.2/z3-4.3.1-BQQcEJY5Khr2mxtgsr1pQ9/libHSz3-4.3.1-BQQcEJY5Khr2mxtgsr1pQ9.a(C.o):(.text+0x12f90): referencia a `Z3_get_parser_error' sin definir
collect2: error: ld returned 1 exit status
`gcc' failed in phase `Linker'. (Exit code: 1)

Sorry for the Spanish error message, but it says that the definitions of functions Z3_get_parser_error, Z3_add_func_interp, ... are not found.

However, in my machine, these functions are declared in the files /usr/include/z3_api.h, and the Z3 library is also available at /usr/lib/libz3.so.

The same problem occurs when using Z3 4.6.0. I also faced the similar problem when compiling the Solidity compiler ethereum/solidity#493.

Could you advise if this is a bug of Z3?

[NikolajBjorner]

Given that the functions that are listed are newer than many other API functions it could suggest that your path contains old builds of Z3 and it is trying to link against these for the newer header definitions.

[ghost]

Thanks for your suggestion. You're right. My machine has an older library of Z3, located at /usr/lib/x86_64-linux-gnu/libz3.so. After deleting this file, I can compile normally.