Your message dated Sun, 25 Aug 2019 14:28:17 +0000 with message-id <e1i1tvb-0006bx...@fasolo.debian.org> and subject line Bug#842892: fixed in z3 4.4.1-1~deb9u1 has caused the Debian Bug report #842892, regarding java.lang.UnsatisfiedLinkError: libz3java.so: undefined symbol: Z3_solver_get_model to be marked as done.
This means that you claim that the problem has been dealt with. If this is not the case it is now your responsibility to reopen the Bug report if necessary, and/or fix the problem forthwith. (NB: If you are a system administrator and have no idea what this message is talking about, this may indicate a serious mail system misconfiguration somewhere. Please contact ow...@bugs.debian.org immediately.) -- 842892: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=842892 Debian Bug Tracking System Contact ow...@bugs.debian.org with problems
--- Begin Message ---Package: libz3-jni Version: 4.4.1-0.3 Severity: important Dear Maintainer, The Java example program included with z3 [1] fails to run. With the package in unstable, the error reported is: 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 is a misleading error (the correct library to load is "z3java", not "libz3java"), caused by hiding an earlier exception [2]. I applied the following patch locally: --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -570,8 +570,9 @@ java_native.write(' public static native void setInternalErrorHandler(long ctx);\n\n') java_native.write(' static {\n') - java_native.write(' try { System.loadLibrary("z3java"); }\n') - java_native.write(' catch (UnsatisfiedLinkError ex) { System.loadLibrary("libz3java"); }\n') + java_native.write(' System.loadLibrary("z3java");\n') + #java_native.write(' try { System.loadLibrary("z3java"); }\n') + #java_native.write(' catch (UnsatisfiedLinkError ex) { System.loadLibrary("libz3java"); }\n') java_native.write(' }\n') java_native.write('\n') With the try-catch removed, the actual exception is revealed: Exception in thread "main" java.lang.UnsatisfiedLinkError: /usr/lib/x86_64-linux-gnu/jni/libz3java.so: /usr/lib/x86_64-linux-gnu/jni/libz3java.so: undefined symbol: Z3_solver_get_model 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:13) at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:86) at JavaExample.main(JavaExample.java:2286) I confirmed that libz3 does in fact export the symbol in question: $ nm -gD /usr/lib/x86_64-linux-gnu/libz3.so | grep Z3_solver_get_model 00000000000a6220 T Z3_solver_get_model It looks like the JNI library is not actually linked against libz3? $ ldd /usr/lib/x86_64-linux-gnu/jni/libz3java.so linux-vdso.so.1 (0x00007ffdc41e7000) libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fb61bcf5000) libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fb61b9f1000) libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fb61b7da000) libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fb61b43c000) /lib64/ld-linux-x86-64.so.2 (0x000055c3b7a27000) [1] http://sources.debian.net/src/z3/4.4.1-0.3/examples/java/JavaExample.java/ [2] http://sources.debian.net/src/z3/4.4.1-0.3/scripts/update_api.py/#L574 thanks, Ryan -- System Information: Debian Release: 8.6 APT prefers stable-updates APT policy: (500, 'stable-updates'), (500, 'proposed-updates'), (500, 'stable') Architecture: amd64 (x86_64) Foreign Architectures: i386 Kernel: Linux 4.7.0-0.bpo.1-amd64 (SMP w/2 CPU cores) Locale: LANG=en_CA.UTF-8, LC_CTYPE=en_CA.UTF-8 (charmap=UTF-8) Shell: /bin/sh linked to /bin/dash Init: systemd (via /run/systemd/system)
--- End Message ---
--- Begin Message ---Source: z3 Source-Version: 4.4.1-1~deb9u1 We believe that the bug you reported is fixed in the latest version of z3, which is due to be installed in the Debian FTP archive. A summary of the changes between this version and the previous one is attached. Thank you for reporting the bug, which will now be closed. If you have further comments please address them to 842...@bugs.debian.org, and the maintainer will reopen the bug report if appropriate. Debian distribution maintenance software pp. Andreas Beckmann <a...@debian.org> (supplier of updated z3 package) (This message was generated automatically at their request; if you believe that there is a problem with it please contact the archive administrators by mailing ftpmas...@ftp-master.debian.org) -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA256 Format: 1.8 Date: Sat, 24 Aug 2019 12:44:04 +0200 Source: z3 Binary: z3 libz3-4 libz3-dev python-z3 libz3-cil libz3-ocaml-dev libz3-java libz3-jni Architecture: source Version: 4.4.1-1~deb9u1 Distribution: stretch Urgency: medium Maintainer: LLVM Packaging Team <pkg-llvm-t...@lists.alioth.debian.org> Changed-By: Andreas Beckmann <a...@debian.org> Description: libz3-4 - theorem prover from Microsoft Research - runtime libraries libz3-cil - theorem prover from Microsoft Research - CLI bindings libz3-dev - theorem prover from Microsoft Research - development files libz3-java - theorem prover from Microsoft Research - java bindings libz3-jni - theorem prover from Microsoft Research - JNI library libz3-ocaml-dev - theorem prover from Microsoft Research - OCaml bindings python-z3 - theorem prover from Microsoft Research - Python bindings z3 - theorem prover from Microsoft Research Closes: 842892 926939 Changes: z3 (4.4.1-1~deb9u1) stretch; urgency=medium . * Non-maintainer upload. * Rebuild for stretch. . z3 (4.4.1-1~deb10u1) buster; urgency=medium . * Non-maintainer upload. * Rebuild for buster. . z3 (4.4.1-1) unstable; urgency=medium . [ Gianfranco Costamagna ] * Team Upload * Upload to unstable . [ Andreas Beckmann ] * Do not set the SONAME of libz3java.so to libz3.so.4. (Closes: #842892) . z3 (4.4.1-0.5~exp1) experimental; urgency=medium . * Package moved to salsa (Closes: #926939) * Standards-Version updated to 4.2.1 * Fix priority-extra-is-replaced-by-priority-optional warning * Moved under the llvm umbrella Checksums-Sha1: e6a95d68cee003db92fc4a926542e95ac9fed657 3051 z3_4.4.1-1~deb9u1.dsc d563fc3173a05c123cca8c962c1d1992f73dbd35 14768 z3_4.4.1-1~deb9u1.debian.tar.xz 9531b8a298eb012e35e11ef2d5f61a05e2afd2d6 20810 z3_4.4.1-1~deb9u1_source.buildinfo Checksums-Sha256: c422411161cbfbbb751e0e910b1da20daf50e99dfd30994f25b0ca1eae9292e3 3051 z3_4.4.1-1~deb9u1.dsc e21d48e2fa9ac9b44fa116e68d0c89ee8331641b337eb5ae455070de50bae706 14768 z3_4.4.1-1~deb9u1.debian.tar.xz 0306b83934fde93554a8554d5da37accd17973c2cacef3f3509d23474677445b 20810 z3_4.4.1-1~deb9u1_source.buildinfo Files: 295cb1f547f6dde079db9a7abe16ce1a 3051 science optional z3_4.4.1-1~deb9u1.dsc 096d57b8c11bfd98a02dd353738edcc6 14768 science optional z3_4.4.1-1~deb9u1.debian.tar.xz 0b1a3ee5e95f4141c26fda11884c2868 20810 science optional z3_4.4.1-1~deb9u1_source.buildinfo -----BEGIN PGP SIGNATURE----- iQJEBAEBCAAuFiEE6/MKMKjZxjvaRMaUX7M/k1np7QgFAl1hFccQHGFuYmVAZGVi aWFuLm9yZwAKCRBfsz+TWentCPTvEACoNpaO4TDPpdxQJwkhLUeiNMsCDB1A36Q2 gQOqubhrFtCNi3Vrx8yAITStY2jRkmMcWfi47qjx4Q00eVW2PKW++sAVM9nPYkfm itZI4hJZ5G0FXOOo1brzMZQ5xA+LJ9d5mRcjkSy60O13ahGDgUVEFNRPOQM2evex Z8ZVrZqMMJS24pP3WgSE1GsMLodAgKd6b2V2sWMO29kbJReCVk8TV5NhYH0pvpBP Gj0Dvu+ozsBotYv2CBQJ44CqosMAiDW0gIYv6bgEexO/fizF223KWj+giVKp6ZtW p6cAWIm8sdXdM93SU06kn/mcx0BMxTG2o1f+q0NSiMtLht6TRfwZK8JnuPv6B/RG WNUwDHPUyTanvuHTn+NN+JLEKYFN/frXwQ7XHNh3k1nzksLNts0ZmUL8tqqsXJpL hOOIuw1TqvLWOgjN/5JU+2/OfQzJFbvyKOHbZd2UHCQCsgV/cPDxcyFa5V0gkiLP mfsTxnfz5jBd+0G9wwRf3qcn2WtXrbtOFgCPMasZ+r4bbRx1PAIy1EJoeHkJbTUY SHrppMw2FiRaNP11Kcbqb2dy66DdRFpJpuf6ZOnSNDYQPr3U2ImAUFazBjOOSUgj gMPias6nTJfLiDi/fZ5NV+U6C7OQMmFSOeL9vZSKrC0noL9rQR3oryIzq6o5mg2Z MjNc+X1tBg== =AUDi -----END PGP SIGNATURE-----
--- End Message ---
