Project

General

Profile

Bug #4066

Binary Windows (x64) product: problems to resolve dependencies of Z3 DLLs

Added by Simon Barner about 2 months ago. Updated 16 days ago.

Status:
Resolved
Priority:
Normal
Assignee:
Category:
-
Start date:
10/05/2020
Due date:
% Done:

0%

Estimated time:

Description

A user experience the below problem when running the DSE.

Analysis:
  • msvcp120.dll + msvcr120.dll could not be resolved despite our DLL pre-loading mechanism
Possible solutions:
  • List VS 2013 redistributable as system requiremet on Win64
  • Add FAQ entry
  • (Deeper analysis on "clean" windows installation (w/o redistributable and msvcp120.dll + msvcr120.dll in the search PATH)
!ENTRY org.eclipse.osgi 4 0 2020-09-24 15:27:22.745
!MESSAGE An error occurred while automatically activating bundle com.microsoft.z3 (6).
!STACK 0
org.osgi.framework.BundleException: Exception in com.microsoft.z3.AF3z3Activator.start() of bundle com.microsoft.z3.
    at org.eclipse.osgi.internal.framework.BundleContextImpl.startActivator(BundleContextImpl.java:863)
    at org.eclipse.osgi.internal.framework.BundleContextImpl.start(BundleContextImpl.java:791)
    at org.eclipse.osgi.internal.framework.EquinoxBundle.startWorker0(EquinoxBundle.java:1015)
    at org.eclipse.osgi.internal.framework.EquinoxBundle$EquinoxModule.startWorker(EquinoxBundle.java:365)
    at org.eclipse.osgi.container.Module.doStart(Module.java:603)
    at org.eclipse.osgi.container.Module.start(Module.java:467)
    at org.eclipse.osgi.framework.util.SecureAction.start(SecureAction.java:493)
    at org.eclipse.osgi.internal.hooks.EclipseLazyStarter.postFindLocalClass(EclipseLazyStarter.java:117)
    at org.eclipse.osgi.internal.loader.classpath.ClasspathManager.findLocalClass(ClasspathManager.java:571)
    at org.eclipse.osgi.internal.loader.ModuleClassLoader.findLocalClass(ModuleClassLoader.java:346)
    at org.eclipse.osgi.internal.loader.BundleLoader.findLocalClass(BundleLoader.java:398)
    at org.eclipse.osgi.internal.loader.sources.SingleSourcePackage.loadClass(SingleSourcePackage.java:41)
    at org.eclipse.osgi.internal.loader.BundleLoader.findClassInternal(BundleLoader.java:472)
    at org.eclipse.osgi.internal.loader.BundleLoader.findClass(BundleLoader.java:425)
    at org.eclipse.osgi.internal.loader.BundleLoader.findClass(BundleLoader.java:417)
    at org.eclipse.osgi.internal.loader.ModuleClassLoader.loadClass(ModuleClassLoader.java:171)
    at java.base/java.lang.ClassLoader.loadClass(ClassLoader.java:522)
    at org.fortiss.af3.exploration.smt.backend.Z3Backend.createSolverRun(Z3Backend.java:117)
    at org.fortiss.af3.exploration.smt.backend.Z3Backend.executeDSE(Z3Backend.java:90)
    at org.fortiss.af3.exploration.service.internal.DSEBackendService$1.run(DSEBackendService.java:176)
    at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
Caused by: java.lang.UnsatisfiedLinkError: C:\Users\schaller\APPs\AutoFOCUS3_Nightly\plugins\com.microsoft.z3_2.17.0.202009230420\lib\x64\msvcp120.dll: Can't find dependent libraries
    at java.base/java.lang.ClassLoader$NativeLibrary.load0(Native Method)
    at java.base/java.lang.ClassLoader$NativeLibrary.load(ClassLoader.java:2442)
    at java.base/java.lang.ClassLoader$NativeLibrary.loadLibrary(ClassLoader.java:2498)
    at java.base/java.lang.ClassLoader.loadLibrary0(ClassLoader.java:2694)
    at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2627)
    at java.base/java.lang.Runtime.load0(Runtime.java:768)
    at java.base/java.lang.System.load(System.java:1837)
    at com.microsoft.z3.AF3z3Activator.loadPluginLocalLibrary(AF3z3Activator.java:65)
    at com.microsoft.z3.AF3z3Activator.start(AF3z3Activator.java:45)
    at org.eclipse.osgi.internal.framework.BundleContextImpl$3.run(BundleContextImpl.java:842)
    at org.eclipse.osgi.internal.framework.BundleContextImpl$3.run(BundleContextImpl.java:1)
    at java.base/java.security.AccessController.doPrivileged(Native Method)
    at org.eclipse.osgi.internal.framework.BundleContextImpl.startActivator(BundleContextImpl.java:834)
    ... 20 more
Root exception:

History

#1 Updated by Johannes Eder 16 days ago

  • Status changed from New to Resolved
  • Assignee changed from Johannes Eder to Simon Barner

Hint as been added to FAQ.

Also available in: Atom PDF