JavaSMT 3.14.0

This minor release comes a new method 'allChar' in String theory
and brings with a smaller bugfix for formula visitation.

JavaSMT 3.13.3

This patch release comes with a smaller bugfix for String-theory formulas in Z3.

JavaSMT 3.13.2

This patch release comes with some updated solvers and some smaller bugfixes.

Updated solvers:

• JavaSMT 2.5-1147-g108647d8
• Z3 4.10.1

JavaSMT 3.13.1

This patch release contains several smaller fixes for the integration of SMTInterpol and Princess.

JavaSMT 3.13.0

This release comes with several bugfixes, e.g., we improved DIV and MOD operations in Integer theory.

Updated solvers:

• MathSAT 5.6.8
• Princess 2022-07-01
• Z3 4.8.17

Breaking change:

The public API for FloatingPointManager was changed to support conversion of FloatingPoint to signed and unsigned Bitvectors.

JavaSMT 3.12.0

This release comes with an initial support for String theory for SMT solvers like Z3 and CVC4. Now, JavaSMT provides statistics on the solving process, depending on the used SMT solver. And we include several bugfixes and internal cleanup.

Breaking change:

The public API was enriched with new methods to retrieve a StringFormulaManager and statistics.

JavaSMT 3.11.0

This release comes with support for multiple prover stacks in SMTInterpol.

Breaking change:

Users might have accessed the public class SmtInterpolEnvironment for direct interaction with SMTInterpol.
We replace the class org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolEnvironment
with the class de.uni_freiburg.informatik.ultimate.logic.Script,
which provides a similar interface and also allows direct interaction with SMTInterpol.

Updated solvers:

• SMTInterpol 2.5-916-ga5843d8b
• Boolector 3.2.2

JavaSMT 3.10.1

This patch release brings several bugfixes for JavaSMT,
for example, in the bindings of Princess or for quantifier handling.
Additionally, we now provide Yices2 via Maven.

Updated solvers:

• SMTInterpol 2.5-842-gfcd46532

JavaSMT 3.10.0

This release contains several improvement, some new features, several bugfixes and updated libraries.
A new method for loading native libraries is available for developers to use their own loading mechanism.
A new method distinct is available for Bitvector formulas.
The visitation of quantified formulas was improved.

Updated solvers:

• Princess 2021-08-12

JavaSMT 3.9.0

This release contains a larger update of Princess and more JUnit tests.
The PrettyPrinter is switched from a boolean parameter to a options enum.
The example projects for Maven are updated with newer solver versions.

Updated solvers:

• Princess 2021-05-10 (improving Array and BV theory, and including a switch to an official Maven repository)