Allow multiple copies of z3 to be loaded into the same process

[bjorn3]

For various reasons it may be possible that multiple copies of z3 are loaded into the same process. If any is loaded with RTLD_GLOBAL all future copies will try to resolve internal symbols in said globally loaded copy even if they are from different versions. This will likely cause errors or even crashes. I can think of two fixes:

• For the python wrapper specifically loading libz3.so with the RTLD_DEEPBIND flag causes glibc's dynamic linker to lookup symbols in the library it is currently loading first before looking in the global scope, thus making multiple copies in use fine.
• Another more general option would be to compile z3 with -fvisibility=protected which should prevent any internally used symbol from being overridden no matter what flags are used during dlopen.

As for why there may be multiple copies of z3 in the first place, in my specific case there was a python program presenting a gui that internally used it's own copy of z3. However before loading this copy of z3 it loaded libGLX.so.0 through QT. libGLX.so.0 then loaded libGLX_mesa.so.0 with RTLD_GLOBAL. libGLX_mesa.so.0 depends on LLVM for compiling shaders, which on Debian depends on libz3.so.4, thus causing another copy of z3 to end up in the global scope.

See https://github.com/angr/angr-management/issues/620 for how this issue was found.

[NikolajBjorner]

Based on the discussion in the commit logs I take we should try to change the setting change in the header file. I don't have a reference to the reason for overwriting the visibility of symbols.

[NikolajBjorner]

this slipped away somehow. I thought the issue was in the header if-def of z3.h and it should be changed. The main question is then the implications of such a change.