Description of problem: When loading the Java bindings for Z3 from the java-z3 package, the class fails to initialize due to its inability to load the native library. (The Java bindings are unusable.) This is not due to the fact that the library is not found, but because the class initialization code calls System.load("libz3java") instead of System.loadLibrary("libz3java"). Note that System.load *must* be called with an absolute path (https://docs.oracle.com/javase/7/docs/api/java/lang/System.html), so the call is invalid, no matter whether the library is on the path. The problem is not in the upstream code, which uses System.loadLibrary. Instead, the file z3.spec in the Fedora source package contains the lines # Comply with the Java packaging guidelines sed -i "s/\(System\.load\)Library/\1/" scripts/update_api.py which replaces System.load by System.loadLibrary. Version-Release number of selected component (if applicable): java-z3-4.4.1-5.fc24.x86_64 (used together OpenJDK 1.8.0_92-b14) How reproducible: Always. Steps to Reproduce: 1. cp /usr/share/doc/z3-doc/examples/java/JavaExample.java . # From package z3-doc 2. javac -cp /usr/lib/java/com.microsoft.z3.jar:. JavaExample.java 3. java -Djava.library.path=/usr/lib64/z3/ -cp /usr/lib/java/com.microsoft.z3.jar:. JavaExample Actual results: This throws: Exception in thread "main" java.lang.UnsatisfiedLinkError: Expecting an absolute path of the library: libz3java at java.lang.Runtime.load0(Runtime.java:806) at java.lang.System.load(System.java:1086) at com.microsoft.z3.Native.<clinit>(Native.java:14) at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:86) at JavaExample.main(JavaExample.java:2286) Expected results: No exception is thrown, the code executes various examples. Additional info: Removing the offending lines from z3.spec probably fixes the problem, but I have not tried it.
I tried the suggested fix (removing the lines from z3.spec). It solves the problem, but it is not obvious, because one still gets an error message about an unsatisfied link error. Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1867) at java.lang.Runtime.loadLibrary0(Runtime.java:870) at java.lang.System.loadLibrary(System.java:1122) at com.microsoft.z3.Native.<clinit>(Native.java:14) at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:86) at JavaExample.main(JavaExample.java:2286) This message is misleading and due to the following loading code: try { System.loadLibrary("z3java"); } catch (UnsatisfiedLinkError ex) { System.loadLibrary("libz3java"); } The second load-library call will fail, because the convention is that the library name must be given without the "lib" prefix. That means that if the first call fails, we will only see the exception of the second call, making it hard to figure out what fails. A hotfix is to put liblibz3java into the library path. I.e., cp /usr/lib64/z3/libz3java.so ./liblibz3java.so java -Djava.library.path=. -cp ~/rpmbuild/BUILD/z3-z3-4.4.1/build/com.microsoft.z3.jar:. JavaExample Now the second call of loadLibrary can work, and we get the actual problem: Exception in thread "main" java.lang.UnsatisfiedLinkError: /home/unruh/tmp/liblibz3java.so: /home/unruh/tmp/liblibz3java.so: undefined symbol: Z3_mk_fpa_numeral_int_uint at java.lang.ClassLoader$NativeLibrary.load(Native Method) at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1941) at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1857) at java.lang.Runtime.loadLibrary0(Runtime.java:870) at java.lang.System.loadLibrary(System.java:1122) at com.microsoft.z3.Native.<clinit>(Native.java:14) at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:86) at JavaExample.main(JavaExample.java:2286) This is because the actual Z3 library (/usr/lib64/libz3.so.0) is not automatically loaded. Ideally, the java-z3 code would already load it (with an added loadLibrary("z3")-call), but we can also do the following: LD_PRELOAD=libz3.so.0 java -Djava.library.path=. -cp ~/rpmbuild/BUILD/z3-z3-4.4.1/build/com.microsoft.z3.jar:. JavaExample Now the file works. (I.e., we get many pages of Z3 related output.)
Thank you for the investigation, Dominique. Your work saved me a lot of time. I've got a fix that works for me in mock. Watch for updates appearing soon.
z3-4.4.1-6.fc23 has been submitted as an update to Fedora 23. https://bodhi.fedoraproject.org/updates/FEDORA-2016-55d7587832
z3-4.4.1-6.fc24 has been submitted as an update to Fedora 24. https://bodhi.fedoraproject.org/updates/FEDORA-2016-ff256fc129
z3-4.4.1-6.fc23 has been pushed to the Fedora 23 testing repository. If problems still persist, please make note of it in this bug report. See https://fedoraproject.org/wiki/QA:Updates_Testing for instructions on how to install test updates. You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2016-55d7587832
z3-4.4.1-6.fc24 has been pushed to the Fedora 24 testing repository. If problems still persist, please make note of it in this bug report. See https://fedoraproject.org/wiki/QA:Updates_Testing for instructions on how to install test updates. You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2016-ff256fc129
z3-4.4.1-6.fc24 has been pushed to the Fedora 24 stable repository. If problems still persist, please make note of it in this bug report.
z3-4.4.1-6.fc23 has been pushed to the Fedora 23 stable repository. If problems still persist, please make note of it in this bug report.