Karlheinz Friedberger

This issue is a good first step towards the next release. Thanks for making the steps transparent.

@leventeBajczi points for noticing ✔️ The tests were just a smaller issue: Please do not disable tests that are intended for all solvers, when just adding one new solver, but...

@leventeBajczi and @baierd : Is there any reason to use Z3 4.5.0 from 07-2016 instead of the latest version with interpolation support from around 05-2018? Was this just an example...

Current status: - Z3 legacy v4.5.0 is available in SVN as dev1-version (only for Linux x64, no Windows or MacOS support, no ARM support). - JavaSMT contains sufficient bindings for...

The current interface for models only supports explicit value assignments. Default values in arrays are not covered by this. The user can query values for array formulas at each required...

@daniel-raffler We did use the Ubuntu docker image (18.04 if possible without further overhead, else the 22.04) for building binary solvers. The steps for publication are documented in https://github.com/sosy-lab/java-smt/blob/master/doc/Developers-How-to-Release-into-Ivy.md#publishing-yices2 ......

With PR https://github.com/sosy-lab/java-smt/pull/526 (especially with the changes here: https://github.com/sosy-lab/java-smt/pull/526/files#diff-7d762d6d2efa9ec5c882c3243c1ed2faf27a21fded89640b90ec5541f8563e87R226-R234 ), we switched from `only` to `rules` and applied other changes from the SoSy-Lab project template. We can take a look...

Hi @cloerkes Thanks for your interest in JavaSMT. Three question, three answers: 1. JavaSMT provides a way to set specific solver-dependent options, in most cases as "solver.SOLVERNAME.furtherOptions". Please see https://[sosy-lab.github.io/java-smt/ConfigurationOptions.txt](https://sosy-lab.github.io/java-smt/ConfigurationOptions.txt)...

This is a rather big API change. This might cause some more changes in CPAchecker than done in https://gitlab.com/sosy-lab/software/cpachecker/-/merge_requests/234 (which is still open and unmerged). I am not convinced that...

I agree with Philipp and would also assume that `totalSize` covers all three components, i.e., exponent, mantissa, and sign bit.