Karlheinz Friedberger

SMTLIB and JavaSMT does not support things like `(x && y) > 2`, but only well-typed expressions like `ITE(x && y, 1, 0) > 2`. Mixing Integer and Boolean logic...

For MathSAT we use an existing DLL from the original development team and then MinGW on Linux to build the bindings for Windows. As Yices also provides the DLL as...

GMP can be build with MinGW on Linux. I have already done that for MathSAT. That's easy.

Are you sure about GMP? The Windows-version is called MPIR. The docu can be found in the script for compiling MathSAT for Windows.

We already use (and used) our own version of Yices for Linux, based on some Git revision of their repository. So, we might stay with always compiling Yices directly. It...

Project started in #162. Not yet finished. The solvers API seems to lack some required features.

### For Linux users: We provide all necessary files in [our Ivy repository](https://www.sosy-lab.org/ivy/org.sosy_lab/). When using Ant/Ivy as build tool, those dependencies are automatically installed. For manual installation, please check the...

A quick initial test showed several problems when compiling the Java bindings for Windows. If really needed, I will investigate further. However, for myself and our group, running other solvers...

Current status: CVC4 dropped support for Java and will re-implement it in the future. Until then we stay with the existing version, which is the revision shortly before they dropped...

There are a few things remaining from JavaSMT's side. I am working on them: - build-scipts updated (nearly done) - loading mechanism fixed (see https://github.com/cvc5/cvc5/pull/9047, or we apply it directly...