No libz3java in java.library.path

For solution (linux only currently) scroll down

While working on the Verifier I came across upon the following error message when trying to run the tests:

java.lang.UnsatisfiedLinkError: no libz3java in java.library.path: /usr/java/packages/lib:/usr/lib64:/lib64:/lib:/usr/lib

	at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2434)
	at java.base/java.lang.Runtime.loadLibrary0(Runtime.java:848)
	at java.base/java.lang.System.loadLibrary(System.java:2015)
	at com.microsoft.z3.Native.<clinit>(Native.java:14)
	at com.microsoft.z3.Context.<init>(Context.java:41)
	at tinycc.logic.solver.z3.Z3Translator.querySatisfiability(Z3Translator.java:180)
	at tinycc.logic.solver.z3.Z3Translator.querySatisfiability(Z3Translator.java:24)
	at prog2.tests.CompilerTests.computeVerificationResult(CompilerTests.java:343)
	at prog2.tests.pub.verify.VerificationTests.testPDFExample(VerificationTests.java:79)
	at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:104)
	at java.base/java.lang.reflect.Method.invoke(Method.java:577)
	at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:59)
	at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
	at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:56)
	at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
	at org.junit.internal.runners.statements.RunBefores.evaluate(RunBefores.java:26)
	at org.junit.internal.runners.statements.FailOnTimeout$CallableStatement.call(FailOnTimeout.java:288)
	at org.junit.internal.runners.statements.FailOnTimeout$CallableStatement.call(FailOnTimeout.java:282)
	at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
	at java.base/java.lang.Thread.run(Thread.java:833)

Trying to fix the issue, I have:

  • Specified an additional argument of -Djava.library.path=/home/nicolase/uni/prog2/project6/libs during running the test, what which only affects the first line of the error message to change to java.lang.UnsatisfiedLinkError: no libz3java in java.library.path: /home/nicolase/uni/prog2/project6/libs
  • Adding an environment variable called DYLD_LIBRARY_PATH with the same path. This does not change the error message
  • (MacOS only) Changing the reference to the libz3.dylib in libz3java.dylib using install_name_tool -change libz3.dylib @loader_path/libz3.dylib libz3java.dylib following the recommendation of this.

This issue does not have the highest priority, as it was possible to circumvent it by using the VM. Only M1 Mac users will still have this issue.

Solution (Linux)

Add an environment varibale calles LD_LIBRARY_PATH with the path to the folder containing the .so files to your execution. (This does not fix it for macOS)

Just to make sure, the libraries are for ARM, not x86, are they (assuming you use M1)? What does Mac OS’ ldd equivalent output when run on these? What does file say? Can you dlopen() (or whatever this is called on :apple: ) them from a C shim?

I actually did not consider this at all. But it seems to be the issue, as both dylib are Non-fat file: libz3java.dylib is architecture: x86_64. (Great error messages :sparkles:)

The new release should have fixed this, as the issue was closed two days ago, but even the new release build just has a x86_64 version of libz3java.dylib, even though libz3.dylib ist compiled as a arm64 library.

M1 Solution

After some more issues (the build scripts is kind of complicated), I now have two dylibs that do the job:
Google Drive Link. Put them into a folder of your choice and set the Enrironment Variable DYLD_LIBRARY_PATH to the path to the directory. (Alternatively specify an additional argument of -Djava.library.path=<your path to the directory>)

Please note, that this library now has a more recent version of z3 than the one used officially (even so far that the Java interface changed a bit), but experimentation so far showed that when using the provided z3 jar on google drive, there were no visible issues.
1 Like