Thanks for the excellent write-up! It is great that we can now run z3 bindings on macOS in the dynamic linking mode. Though I think it still should be possible to get away with the ABI problem in the static mode.
The links do not work, could you please update them? I presume that the problem arises from the ABI mismatch due to the use of the code units built by different compilers. We have to be sure that we build z3 with the same compiler that was used to build the dependencies (e.g., libc++). We can achieve it either by properly selecting the dependencies (e.g., we can select between libstdc++ and libc++) or by selecting a compiler that is building z3 (clang++ vs g++). It is a fundamental issue that is not actually specific to z3, but rather to C++. For example, in BAP we have the same problem with loading llvm and we solve it by ensuring that we use clang++ and libc++ on macOS. Now, when I review my own patch, I am wondering why have I hardcoded libstc++. It is definitely a shortcoming and in general, we should be careful in selecting the C++ library (again it should be the function of the compiler that is used to build z3 and the compiler itself should be selectable as well).
Besides, have you tried building z3 using clang++ and dynamically linking with libc++? I believe it should resolve the ABI mismatch problem.
Bravo indeed! But we have also to consider the dlopen loader, which commonly has a more strict behavior than the operating system dynamic loader. It doesn’t allow any unresolved symbols that is why we (BAP) prefer statically linking the dependencies into cmxs files, so that we can be sure that they are loaded in runtime without any problems.
P.S. to be honest I stopped using macOS for development as they make the programmers’ life harder with each new release. I am currently lagging five versions behind, sill on El Captain 
P.P.S and also there is Windows, and flexdll, which adds a couple more of dimensions to the problem.