Your message dated Sun, 25 Aug 2019 14:27:50 +0000 with message-id <[email protected]> and subject line Bug#842892: fixed in z3 4.4.1-1~deb10u1 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 [email protected] immediately.) -- 842892: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=842892 Debian Bug Tracking System Contact [email protected] 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~deb10u1 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 [email protected], and the maintainer will reopen the bug report if appropriate. Debian distribution maintenance software pp. Andreas Beckmann <[email protected]> (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 [email protected]) -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA256 Format: 1.8 Date: Sat, 24 Aug 2019 12:18:35 +0200 Source: z3 Architecture: source Version: 4.4.1-1~deb10u1 Distribution: buster Urgency: medium Maintainer: LLVM Packaging Team <[email protected]> Changed-By: Andreas Beckmann <[email protected]> Closes: 842892 926939 Changes: 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: 688787d5afaccd7c30b9a63012a50416c6c114aa 3055 z3_4.4.1-1~deb10u1.dsc ab83a33d32ef56c3907bf3571e53a5817d717b66 14716 z3_4.4.1-1~deb10u1.debian.tar.xz e68afa1a134d925431437782818c0857b978773d 19930 z3_4.4.1-1~deb10u1_source.buildinfo Checksums-Sha256: f9255527c446de49228c37ad209bdf622e3f08cc25b1da25ff65d6c17e672d52 3055 z3_4.4.1-1~deb10u1.dsc 970648b0924b4fea16dce08d3f2f95048c8ef5175bfefd27c4101386898cb218 14716 z3_4.4.1-1~deb10u1.debian.tar.xz 32ea1e6254ed6f6cdc61e69b867d103e9e2ab36fd24ac5c6176200383b79af10 19930 z3_4.4.1-1~deb10u1_source.buildinfo Files: bc0e5c4032a44e440193dea14f857aac 3055 science optional z3_4.4.1-1~deb10u1.dsc ba2cf970d031bd52cf4b759d66363263 14716 science optional z3_4.4.1-1~deb10u1.debian.tar.xz 70e83641cf047fe36c9d70376f77f298 19930 science optional z3_4.4.1-1~deb10u1_source.buildinfo -----BEGIN PGP SIGNATURE----- iQJEBAEBCAAuFiEE6/MKMKjZxjvaRMaUX7M/k1np7QgFAl1hFEsQHGFuYmVAZGVi aWFuLm9yZwAKCRBfsz+TWentCDXwEACmno+i53f+GjmaTOTV5VTagEGfv6Gzkbu2 IfkKD1LJQPMX5IRx9DfE1VG5l8q1qEtXlVljkYinxh7RzEfx9zxFz18RSleeyRZ4 zqNEPaoxS2G/Bnfql6R4LsABoDtJqFj13u9xKerAnAS+pIk3EBrJPHplpCGOYsFO xW8ytfeOVgcvMA5jTpvs8CHI5aOw3ZhgAe+gaEQOKyKqOT78XfWni2gDeyExVuFk GhJ5I6x9XanqDQ7kxOgdReMgJhJ3CzMP7GcoUpt8m18z/jBwcXOXiVCZpBViHCdN CX+yyb8TCyK1C8zYtbbaAV4bQ9ABaqaay2Zx7rRkGAuNR9QN9os0fwAsQTHiCA0/ r8QMJ2Aw186umK3E2QFLn5lyzoHERcm41ZqOIjjB5V+BnmDuUNgDc5SzlUUkAglb i4cqErhhMK0smusb7qIDb/xzzMp3NLf4kMnJFtGuzeonwWvlHPkgRRfY9aJHrgaQ 4rzxGKr6ZR+xDXU+7qOwDrBCSxA/XTCUlzWdNFwTyFLTLL3uJ+59WxrLy0tTwK2e SUkn/Rqc0FvAiBHSKOzjI1JIe6/YicyATIoIWRhWWijMFwFdlyVvHrsYYDhWIsXY s/6JUMvH2i6/41z+02jH8/LBgDk45Mmew9w00novPjuANZEzewElaFrspPcf1Qvv MKf0a6v7SA== =8IKE -----END PGP SIGNATURE-----
--- End Message ---
