Binary Windows (x64) product: problems to resolve dependencies of Z3 DLLs
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:
(from redmine: issue id 4066, created on 2020-10-05)