Z3 Java in eclipse (MacOS)

Sep 11, 2014 at 1:38 PM
Hey,

I've some difficulties to get the JavaZ3 running within a eclipse project. The error message what i get is the following:

java.lang.UnsatisfiedLinkError: no z3java in java.library.path
at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1764)
at java.lang.Runtime.loadLibrary0(Runtime.java:823)
at java.lang.System.loadLibrary(System.java:1044)
at com.microsoft.z3.Native.<clinit>(Native.java:10)
at com.microsoft.z3.Context.<init>(Context.java:24)
at test.org.fortiss.af3.scheduling.z3lib.Z3JavaAPITests.firstTest(Z3JavaAPITests.java:41)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:597)
at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:47)
at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:44)
at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
at org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:271)
at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:70)
at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:50)
at org.junit.runners.ParentRunner$3.run(ParentRunner.java:238)
at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:63)
at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:236)
at org.junit.runners.ParentRunner.access$000(ParentRunner.java:53)
at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:229)
at org.junit.runners.ParentRunner.run(ParentRunner.java:309)
at org.eclipse.jdt.internal.junit4.runner.JUnit4TestReference.run(JUnit4TestReference.java:50)
at org.eclipse.jdt.internal.junit.runner.TestExecution.run(TestExecution.java:38)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:467)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:683)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.run(RemoteTestRunner.java:390)
at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.main(RemoteTestRunner.java:197)
I have a com.microsoft.z3 package where i have com.microsoft.z3.jar in the referenced libraries.
IN https://z3.codeplex.com/discussions/451539 I have read about setting the LD_LIBRARY_PATH. I was trying to do so by right clicking to "Referenced Libraries" (in the com.microsoft.z3 package) and adding a new variable. This variables was pointed to the "build" folder of z3, where one can find the libz3java.dylib files. This didnt really help.

If I compile the example the way it was described in the help, it seems to work:
java -cp com.microsoft.z3.jar:. JavaExample

For that i ve to be in the build folder though.

So could you maybe tell me what I ve to do to be able to use the z3 java api in my eclipse projects?

I use MacOS 10.9.3 and Eclipse Kepler
Coordinator
Sep 11, 2014 at 3:41 PM
The com.microsoft.z3.jar package depends on both, libz3.dylib (the actual native library) and libz3java.dylib (the translation JNI library). Both can be found in the build directory after a successful build. At runtime, those libraries need to be visible either through DYLD_LIBRARY_PATH (which is the name for LD_LIBRARY_PATH on OSX), or through the Java VM option -Djava.library.path=c:\path\to\z3\build
Sep 11, 2014 at 3:50 PM
Hey,

I added to my run configurations -> VM Arguments: -Djava.library.path=/Users/username/Desktop/javaz3api/z3/build

I'm still getting the error .. what am I doing wrong?
Coordinator
Sep 11, 2014 at 4:30 PM
I just tried with a fresh project and I got a different error. libz3java.dylib references libz3.dylib but when that happens it doesn't look into the java library path, so I had to add both, -Djava.library.path=/path/to/z3 and also DYLD_LIBRARY_PATH=/path/to/z3 in the "environment" tab of the project run/debug configurations.
Sep 12, 2014 at 8:02 AM
That works, thank you.