Karlheinz Friedberger

Please report this issue to Yices. If they provide a fix, we can update the library in JavaSMT quite easily. Also, using a formula visitor to print a formula (and...

We appreciate your patience and understand the requirement. At the moment, our team lacks deep expertise with macOS and also the corresponding hardware. Getting started on this will likely require...

We discussed that topic with the MathSAT developers years ago and I thought that they fixed the issue. It was some bug in evaluating UFs and arrays in the model....

There is a new version of MathSAT 5.6.12 available. However, it seems that it was compiled on newer GLIBC and our build-scripts and Docker images are not sufficient. We either...

I also thought about providing a fat JAR via Maven, depending on architecture (x64 vs arm64), operating system (Linux vs Windows vs MacOS) and licence (GPL-included vs non-GPL). This would...

There should be no need to copy dependencies (or create symlink) in a user-sided application. The copy- or symlink-approach is only required for internal development in JavaSMT itself. Other projects...

The availability of CVC5 on Windows is currently waiting on PR https://github.com/sosy-lab/java-smt/pull/454 . We still try to minimize the number of dependencies and libraries required by CVC5, e.g., by static...

We updated CVC5 as dependency in our development (master) branch. This is not synchronized with any already released version. There are several ways that your installation receives the newest version...

**Update:** Intermediate version `java-smt-5.0.1-523-g9001c0ea4` was released to ivy and Maven. It contains references to the latest solver integration.

Windows does not support proper symlinks. Thus, I assume that your depentent native libraries in the directory 'lib/native' are outdated. Please cleanup that directory, e.g. remove all so-files, and then...