z3 icon indicating copy to clipboard operation
z3 copied to clipboard

java.lang.UnsatisfiedLinkError at MacOS with JavaExample.java

Open sabrieker opened this issue 7 months ago • 2 comments

I executed below commands but couldn't figure out why it fails.

OS: MacOS Sequoia 15.4.1 (24E263) JDK : java --version Picked up JAVA_TOOL_OPTIONS: -Duser.language=en -Duser.country=US openjdk 17.0.2 2022-01-18 OpenJDK Runtime Environment Homebrew (build 17.0.2+0) OpenJDK 64-Bit Server VM Homebrew (build 17.0.2+0, mixed mode, sharing)

cd /Users/theuser/microsoft
git clone https://github.com/Z3Prover/z3.git
cd /Users/theuser/microsoft/z3
python3 scripts/mk_make.py --java
cd build
make -j4 

cp /Users/theuser/microsoft/z3/examples/java/JavaExample.java .
javac -cp /Users/theuser/microsoft/z3/build/com.microsoft.z3.jar:. JavaExample.java 
java -Djava.library.path=/Users/theuser/microsoft/z3/build/ -cp /Users/theuser/microsoft/z3/build/com.microsoft.z3.jar:. JavaExample

Error Stacktrace

 build % java -Djava.library.path=/Users/theuser/microsoft/z3/build/ -cp /Users/theuser/microsoft/z3/build/com.microsoft.z3.jar:. JavaExample
Picked up JAVA_TOOL_OPTIONS: -Duser.language=en -Duser.country=US
Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path: /Users/theuser/microsoft/z3/build/
	at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2429)
	at java.base/java.lang.Runtime.loadLibrary0(Runtime.java:818)
	at java.base/java.lang.System.loadLibrary(System.java:1989)
	at com.microsoft.z3.Native.<clinit>(Native.java:17)
	at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:87)
	at JavaExample.main(JavaExample.java:2285)

sabrieker avatar May 08 '25 14:05 sabrieker

Is java binding still using the mk_make or shifting to cmake?

arbipher avatar Jul 03 '25 22:07 arbipher

You can build java with cmake and my recollection is that it offers a more reliable install experience.

When it comes to releases: release.yaml uses mostly mk_make, still. It uses cmake for Windows ARM. nightly.yaml uses cmake for Windows.

NikolajBjorner avatar Jul 03 '25 23:07 NikolajBjorner