Z3Prover
about the maven dependence，can not run normal
I use the maven add this dependence
<dependency> <groupId>org.sosy-lab</groupId> <artifactId>javasmt-solver-z3</artifactId> <version>z3-4.4.1-1558-gf96cfea</version> </dependency>
use the function of examples like this：
`public void simpleExample()
{
System.out.println("SimpleExample");
try {
Log.open("SimpleExample");
Log.append("SimpleExample");
}catch (Exception e){
e.printStackTrace();
}finally{
Log.close();
}
{
Context ctx = new Context();
/* do something with the context */
/* be kind to dispose manually and not wait for the GC. */
ctx.close();
}
}`
about the Native.java
report the error：java.lang.NoClassDefFoundError: Could not initialize class com.microsoft.z3.Native I don't know how to deal with the error。
please help me，thank you
This sounds like a problem with a Maven package. The problem is almost surely that your system cannot find libz3.so/.dylib/.dll at runtime, which is either because some of the paths are not set up correctly, or there is a mismatch between your system bitness (32/64 bit) and Z3. We do not manage that entry in Maven, however.
@cheshire: Is it correct that you are the maintainer of the Z3 entry at mvnrepository.com? If so, could you advise? Also, there's a typo in my name in there, but ideally I don't want to be listed as a contact at all as I don't/can't maintain those packages.
@GOGJIAN the package only provides the binaries for 64 bit Linux, are you on that platform? @wintersteiger I had setup that package, yes, but unfortunately I can not maintain it at the moment. We can explore a number of options here:
- I could take it down entirely
- I could pass the ownership to you
- I could ask current maintainers of JavaSMT to see whether they would be willing to support the package In general, Maven does not directly support handling binaries, and doing that requires going through the hoops.
Hello, I just wanted to know if you ever found a solution to this issue
There is no support for Maven related issues. But you are invited to submit a solution.
If providing a build system wrapper to CMake like sbt/mill, would it be possible to PR this wrapper, making it possible to give a Maven release? Or if not possible, would it be possible to release a jar in GitHub release, so that we can download this jar from official release.
Sure, the azure-pipelines.yml script runs builds on checkins and the "release.yml" and "nightly.yml" publish packages. If you have a packaging solution it should be possible to add it to these pipelines through a pull request.
Sorry for the delay, I'm totally missed this notification.
I think z3/src/api/java/CMakeLists.txt needs some rework, using standard java specified build system to manage the java code, and use the plugin to publish it. I'm a Scala guy, so only familiar with sbt and mill, not sure are these tool acceptable by upstream.
A rule of thumb for acceptable tools for upstream are the ones listed as already included in packages: https://docs.microsoft.com/en-us/azure/devops/pipelines/agents/hosted?view=azure-devops&tabs=yaml For example, I see sbt. Adding other goodies is less easy. For example, Z3 releases ocaml bindings but the Windows support for ocaml was never on par with Linux/BSD and it is additional friction every time I have to touch the ML bindings.