Karlheinz Friedberger

Z3 was published to Ant/Ivy and Maven in versions 4.13.2 and 4.13.3. There are some smaller issues that are currently blocking this PR from merging: - JavaSMT uses outdated CI...

This branch is currently blocked by or waiting for: - Z3 for Windows is broken on a default WIndows installation due to unexpected changes in msvcp140.dll. We need to wait...

I would like to have a preliminary review for these changes. The following parts are work in progress and could be solved later: - CI for ARM, for Linux, Windows,...

@daniel-raffler and @baierd : could you take a look and provide feedback? I would like to merge this PR in near time. Beside Java-based solvers SMTInterpol and Princess, we now...

I would not expect such a info-feature from a library, but only in the main application.

For executing and testing the ARM-based binaries, you can apply Podman/Docker with Qemu. A corresponding Dockerfile would look like this: ``` FROM arm64v8/ubuntu:22.04 ENV DEBIAN_FRONTEND=noninteractive ENV TZ=UTC ENV LANG=C.UTF-8 RUN...

The Podman/Docker file might be interesting for additional CI jobs. We will surely come across that topic in https://github.com/sosy-lab/java-smt/issues/384.

As a first step, we improved the support for Linux with additional configurations for arm64 architecture in #442 .

JavaSMT does not want to introduce additional utility symbols and equations. Integrating this functionality directly within Princess/Ostrich would be beneficial. This enhancement is not a high priority for us, so...

Does this issue only affect simple formulas like ` |(|` or also complex ones like `and |(| x |)|`?