Bug#842892: marked as done (java.lang.UnsatisfiedLinkError: libz3java.so: undefined symbol: Z3_solver_get_model)

2019-08-25 Thread Debian Bug Tracking System 
Your message dated Sun, 25 Aug 2019 14:28:17 +
with message-id 
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.(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.(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
000a6220 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 (0x7ffdc41e7000)
libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 
(0x7fb61bcf5000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x7fb61b9f1000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 
(0x7fb61b7da000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x7fb61b43c000)
/lib64/ld-linux-x86-64.so.2 (0x55c3b7a27000)

[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  (supplier of updated z3 package)

(This mes

Bug#842892: marked as done (java.lang.UnsatisfiedLinkError: libz3java.so: undefined symbol: Z3_solver_get_model)

2019-08-25 Thread Debian Bug Tracking System 
Your message dated Sun, 25 Aug 2019 14:27:50 +
with message-id 
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 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.(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.(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
000a6220 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 (0x7ffdc41e7000)
libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 
(0x7fb61bcf5000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x7fb61b9f1000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 
(0x7fb61b7da000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x7fb61b43c000)
/lib64/ld-linux-x86-64.so.2 (0x55c3b7a27000)

[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 842...@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Andreas Beckmann  (supplier of updated z3 package)

(This m

Bug#842892: marked as done (java.lang.UnsatisfiedLinkError: libz3java.so: undefined symbol: Z3_solver_get_model)

2019-08-17 Thread Debian Bug Tracking System 
Your message dated Sat, 17 Aug 2019 10:50:35 +
with message-id 
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 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.(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.(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
000a6220 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 (0x7ffdc41e7000)
libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 
(0x7fb61bcf5000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x7fb61b9f1000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 
(0x7fb61b7da000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x7fb61b43c000)
/lib64/ld-linux-x86-64.so.2 (0x55c3b7a27000)

[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 842...@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Gianfranco Costamagna  (supplier of updated z3 
package)

(This message was