Your message dated Sat, 17 Aug 2019 10:50:35 +0000 with message-id <[email protected]> and subject line Bug#842892: fixed in z3 4.4.1-1 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 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. Gianfranco Costamagna <[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, 17 Aug 2019 11:05:53 +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 Distribution: unstable Urgency: medium Maintainer: LLVM Packaging Team <[email protected]> Changed-By: Gianfranco Costamagna <[email protected]> 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 Changes: 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) Checksums-Sha1: 186e3e4fa864d21854caf73c49436d20c1d1130c 2998 z3_4.4.1-1.dsc 4115d684c5a0ee7ad47cb1db01ae4137a37cc67e 14660 z3_4.4.1-1.debian.tar.xz cb3447190f569139edb1b157adfff86ce0d9fa9f 22052 z3_4.4.1-1_source.buildinfo Checksums-Sha256: ad397450bfb8be8c9431dc7294a9df1b305da70e2445b96f2ae696dd16beb82a 2998 z3_4.4.1-1.dsc b34338af7779d9a661a1e3509360ade98e2e47eeccccf3e0047e4e1d00c146ae 14660 z3_4.4.1-1.debian.tar.xz 383dad5c627bcf470b476ec843cc1ea93d0c673d52309cd8be9fa0ab18b3def4 22052 z3_4.4.1-1_source.buildinfo Files: b52e9f6b14e762dc05ed39a8e9c4657b 2998 science optional z3_4.4.1-1.dsc 70d722ae3ef02ec5fc4af54f438c9e2f 14660 science optional z3_4.4.1-1.debian.tar.xz d93beeb7f058c46483555c07a2fb95dc 22052 science optional z3_4.4.1-1_source.buildinfo -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEEkpeKbhleSSGCX3/w808JdE6fXdkFAl1Xw8QACgkQ808JdE6f XdmEJxAAvIb2fjlcZ4eNkWAWiuEIwzCoKwYJxv2eXCVR5JEwPgsnuc5xLM0ITaGd c/5iFVBtNNRGsT8XEmDrYbEpPLFs0Yu8T38cBk3JUOpUBzR0DD2epo+7Q+Qr5QfL BOoWPUcEbpIzeqGUTyBVayQyKiE67quiaw+yCJLB6ARq6MqwL30G0GO8PE4OrYwc gr1UMuzLyigeoTt7Ynj9eulLY3qcxsUJwRrpx1dQwjFdkEXW9o7cbTcOqzJQXiYc 5K/zC63hqLDBWnkUZRF7oup6lWV/pCKfHn/COUz0C5kJInGVbXXjl6/yF46xscLx EFW/etJ5UMFkMdWpvUqMzsOu9V5paHyJSWCbDGTr9EPq7bLOdhbxMRQu2PgsgE+V tV2i2fs/jInJEaluafiTSMUJZ2qFZrgkf4WSK12zP5psH27gJP88jKvTKEhvZRty zEwMg7ktt/MLML/93Y84iSTOXqNK79rYoZLzykS8tb+TM64dvWQKboVJMBT11edM dFMX8ZSGyaTPET9rGs+o5DJH4KbL+6AMkkAgdAZRTmCOy7NYB3YeC9FGi8GIe2d/ Oespl4JKBVBMaEmjtoLNIQy9qi6RyIRRsqqOSbQgItpYhpi3Xz4EpuE7+BCQbSzh y07F4JbIWgKp8blbQZhjmvNI1VhwN67ycLaWFZrZZyS9FLCxpaU= =6mbX -----END PGP SIGNATURE-----
--- End Message ---
