z3 java API fails to detect libz3.dylib on BigSur

[polgreen]

Hi,

I'm using z3 java bindings in a project (https://github.com/uclid-org/uclid) on Big Sur 11.1, and I think I am running into issue #294 again:

I've tried the solution in that thread, which worked on my intel mac on Mojave and Catalina with openJDK11 (and also openJDK8 but it didn't work with a later version of openJDK):

    put JNI dynamic link libraries in:              /Library/Java/Extensions
    e.g. libz3java.dylib
    put none-JNI dynamic link libraries in:     /usr/local/lib
    e.g. libz3.dylib

As far as I can tell, this solution doesn't work on BigSur and I get the error:

Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path
	at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1875)
	at java.lang.Runtime.loadLibrary0(Runtime.java:872)

The only way I can fix this error is to put libz3.dylib in the same directory that I call the binary from (I can leave libz3java.dylib in /Libary/Java/Extensions).

I've recreated this on two different setups:

• BigSur 11.1 on an M1 macbook, with zulu openjdk version 1.8.0_282 , and z3 4.8.11
• BigSur 11.1 on an intel macbook with AdoptOpenJDK11 and z3 4.8.8

Has anyone else encountered this and got a solution?

[mmuesly]

Hi @polgreen,

together with @no-preserve-root, I maintain an artifact called z3-turnkey: https://github.com/tudo-aqua/z3-turnkey

Today, I worked on bouncing the included binaries to z3-4.8.10, but it is still work in progress. Something is not working on the linux side at the moment. Hopefully, I can fix it in the next couple of days.

We had to run install_name_tool -change libz3.dylib @loader_path/libz3.dylib in the process to make the library loadable with dependencies on osx.

The otool output changed as follows:
Default build:

 > otool -L libz3java.dylib 
 libz3java.dylib:
	libz3java.dylib (compatibility version 0.0.0, current version 0.0.0)
	libz3.dylib (compatibility version 0.0.0, current version 0.0.0)
	/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 902.1.0)
	/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1281.100.1)

to z3-turnkey version:

otool -L libz3java.dylib 
libz3java.dylib:
	libz3java.dylib (compatibility version 0.0.0, current version 0.0.0)
	@loader_path/libz3.dylib (compatibility version 0.0.0, current version 0.0.0)
	/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 902.1.0)
	/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1281.100.1)

Now, the loader should look for the related libz3.dylib next to the libz3java.dylib.

No prefix means, that it should be in the same folder as the binary loading the library. Therefore, the default builds should work the way you described it but has no chance to finde the library anywhere else on the system.

We load the library from a tmp folder as described in this method.
Making the changes to the loading path, I got full access to Z3 through the Java-API and dependency loading worked smoothly on MacOS 11.2 with OpenJDK 11.0.2 today.

Eventually, this might give you some hints to resolve the issue on your machine.