Bug#842892: java.lang.UnsatisfiedLinkError: libz3java.so: undefined symbol: Z3_solver_get_model

[crtmike at gmail.com]

Control: severity -1 grave

It's frustrating to see a bug report being ignored for nearly three
years. The severity is definitely release-crtical, because it renders
this package (libz3-jni) unusable.

PS: I tried to patchelf the .so file in question. The result, however,
is ridiculous.

$ sudo patchelf --set-soname "whatever" /usr/lib/x86_64-linux-
gnu/jni/libz3java.so
$ ldd /usr/lib/x86_64-linux-gnu/jni/libz3java.so
	linux-vdso.so.1 (0x00007ffe4cd46000)
	XXXXXXXXXX => not found
	libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6
(0x00007fb5d29ac000)
	libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6
(0x00007fb5d2829000)
	libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1
(0x00007fb5d280f000)
	libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6
(0x00007fb5d264e000)
	/lib64/ld-linux-x86-64.so.2 (0x00007fb5d2bc2000)

Well, at least you can turn to LD_PRELOAD instead of patchelf.

If you are bit by this Debian-specific bug, stop here. Download the
official binaries and simply set LD_LIBRARY_PATH, unless somebody fixes
this bug, whose root cause is already known 3 years ago, thanks to
Andrey. Let's hope the fix does not take another 3 years...