Christoph M. Wintersteiger

We can't distribute fully compiled and linked .jar files for all platforms, but it would indeed be nice if the build system would automatically put everything into one .jar file...

Thanks for the comment @cheshire, I agree with you too. Some people are thinking about or working on binary packages for various systems which for many users will mean that...

I don't know. What's Ivy? In general pulibshing packages is encouraged, as long as the maintainer is actually doing the maintenance. I have no idea about Ivy and the conditions...

Thanks for the info! Sure, sounds good to me as long as this isn't a one-shot event where a binary is pushed but never updated. You seem to be using...

I think it should be within it's own "Z3 Theorem Prover" organization, not necessarily under Microsoft (just like it is on GitHub; it's neither in [Microsoft](https://github.com/Microsoft) nor in [Microsoft Research](https://github.com/MicrosoftResearch))....

I've never considered that partciluar use case, but if you can call the native functions that should be just fine as long as you make sure all terms are correctly...

Indeed, you'd have to know the context. Currently there are no public facilities for constructing other objects, because we've never needed them. The reason all the constructors are internal/private is...

I haven't looked at this in far too long, so this may have changed. I think the reason for using finalizers was that they can be re-scheduled if the underlying...

@rainoftime The "bit-blasting bit-vector solver" is not a single, isolated piece of code. It is implemented via multiple preprocessing tactics (i.e. you need the complete tactic framework), then the SAT...

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...