Description
JavaSMT when used via Ivy or Maven depends on an SMTInterpol JAR that contains not only classes from SMTInterpol, but instead also from several libraries of the Ultimate project (e.g., classes in de.uni_freiburg.informatik.ultimate.logic etc.). This causes a problem for users of JavaSMT that also use other components that depend on these Ultimate libraries, because duplicate classes end up on the class path and hard-to-find bugs may occur. An example of a problem this caused is https://gitlab.com/sosy-lab/software/cpachecker/-/issues/915.
Furthermore, such JARs that contain classes from several independent components also conflict with the module system of Java 9 (such JARs work on the classpath but not on the module path).
Packaging (transitive) dependencies into one's own JAR file is an anti pattern for libraries due to these problems. And in fact, for those who use JavaSMT via Ivy or Maven there is not a single advantage to having everything inside a single JAR, because the dependency manager will handle all the (transitive) dependencies anyway, so it doesn't matter for the user if SMTInterpol is just a single JAR or whether it has a dozen dependencies. But in the latter case the dependency manager can warn and maybe even resolve conflicts.
So please make JavaSMT's SMTInterpol dependency avoid having bundled dependencies and instead declare them as proper dependencies. (There is no problem with keeping JARs with the full dependencies included available for other users, of course.)
An alternative implementation for a solution would be shading of dependencies: Renaming all classes of the dependencies into one's own namespace and then packaging them together with one's own classes in the JAR. This has an effect similar to static linking, because the main classes will always use the bundled dependencies (in the exact same version), no matter what else exists on the class path. There are tools for this that do this automatically while creating JARs (e.g., the Maven Shade Plugin).