I have a perfectly working Z3 Build system for Java. I want to call it from an Eclipse plugin. I tried several approaches, but non of them are working for me. These approaches are:
- Adding Z3 build as an external class folder How to Use External Class Files in an Eclipse Project
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:87) at TestZ3.main(TestZ3.java:9)
- Copied Z3 build to the Eclipse plugin, at the root. Then added com.microsoft.z3.jar under the Libraries (Right-mouth click on the project->Build Path->Configure Build Path->Libraries->Add Jars). The error is:
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:87) at plugintest.handlers.SampleHandler.execute(SampleHandler.java:37) at org.eclipse.ui.internal.handlers.HandlerProxy.execute(HandlerProxy.java:295) at org.eclipse.ui.internal.handlers.E4HandlerProxy.execute(E4HandlerProxy.java:90) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62) at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43) at java.lang.reflect.Method.invoke(Method.java:498) at org.eclipse.e4.core.internal.di.MethodRequestor.execute(MethodRequestor.java:56) at org.eclipse.e4.core.internal.di.InjectorImpl.invokeUsingClass(InjectorImpl.java:252) at org.eclipse.e4.core.internal.di.InjectorImpl.invoke(InjectorImpl.java:234) at org.eclipse.e4.core.contexts.ContextInjectionFactory.invoke(ContextInjectionFactory.java:132) at org.eclipse.e4.core.commands.internal.HandlerServiceHandler.execute(HandlerServiceHandler.java:152) at org.eclipse.core.commands.Command.executeWithChecks(Command.java:493) at org.eclipse.core.commands.ParameterizedCommand.executeWithChecks(ParameterizedCommand.java:486) at org.eclipse.e4.core.commands.internal.HandlerServiceImpl.executeHandler(HandlerServiceImpl.java:210) at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.executeItem(HandledContributionItem.java:799) at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.handleWidgetSelection(HandledContributionItem.java:675) at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.access$7(HandledContributionItem.java:659) at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem$4.handleEvent(HandledContributionItem.java:592) at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84) at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4362) at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1113) at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:4180) at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3769) at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$4.run(PartRenderingEngine.java:1127) at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337) at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1018) at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:156) at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:694) at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:337) at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:606) at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:150) at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:139) at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196) at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:134) at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:104) at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:380) at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:235) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62) at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43) at java.lang.reflect.Method.invoke(Method.java:498) at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:669) at org.eclipse.equinox.launcher.Main.basicRun(Main.java:608) at org.eclipse.equinox.launcher.Main.run(Main.java:1515) at org.eclipse.equinox.launcher.Main.main(Main.java:1488)
- With or without the previous step, I added com.microsoft.z3.jar to Classpath, located at the Plugin.xml Runtime tab. In this case, the plugin is not finding the handler that is invoked after button press command.
!MESSAGE plugintest.handlers.SampleHandler cannot be found by PluginTest_1.0.0.qualifier !STACK 0 java.lang.ClassNotFoundException: plugintest.handlers.SampleHandler cannot be found by ....more
In fact, this approach worked for me a previous a installation (Dell, Intel, x64, Eclipse Mars (x64), Java 1.8 x64)!
- Following the discussion in https://github.com/Z3Prover/z3/issues/1093, I configured Native Library Location of com.microsoft.z3.jar with the Z3 Build directory. Calling the Z3 Build from Eclipse plugin, the error reported is the same as in Approach 2, but calling it from a Java application, the error is more specific:
Exception in thread "main" java.lang.UnsatisfiedLinkError: C:\Users...TestZ33\build\libz3java.dll: Can't find dependent libraries 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:14) at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:87) at TestZ3.main(TestZ3.java:9)
What is working is when you have a Java application under the Z3 build directory. Can anyone help how to use the Z3 build directory from a Java application, or from Eclipse plugin. By the way, I followed approach #2, was working fine until I try to replicate it (because my laptop crashed) and forced to use another laptop, then the same procedure is not working for me (I had luck, before). Right now, the new laptop has the following settings:
HP Laptop (AMD, x64)
C:\Users\nmd02\git\resa_mars_workspace>java -version
java version "1.8.0_144"
Java(TM) SE Runtime Environment (build 1.8.0_144-b01)
Java HotSpot(TM) 64-Bit Server VM (build 25.144-b01, mixed mode)
PATH:
%SystemRoot%\system32;%SystemRoot%;%SystemRoot%\System32\Wbem;%SYSTEMROOT%\System32\WindowsPowerShell\v1.0\;C:\Program Files (x86)\QuickTime\QTSystem\;C:\Program Files\MATLAB\2017a\runtime\win64;C:\Program Files\Java\jdk1.8.0_144\bin;C:\Program Files\Git\cmd;C:\Program Files\CMake\bin;C:\MinGW\bin;C:\python36;C:\Users...git\ninja;C:\Program Files (x86)\Windows Kits\8.1\Windows Performance Toolkit\;C:\gnuwin32\bin
I really appreciate for your help in advance.
Cheers, /Nas
