JavaSMT 3.8.0

This release contains smaller bugfixes, some cleanup, and updated libraries.

Updated solvers:

• MathSAT5 5.6.6
• Z3 4.8.10

JavaSMT 3.7.0

This release contains the first official support for native SMT solvers on Windows.
We provide MathSAT5 and Z3 for Windows (64bit) as part of the Ivy build.
A user can of course exclude the native libraries from the dependencies,
if disk space is a critical point.

Updated solvers:

• MathSAT5 5.6.5 (inculding binary for Windows)
• Z3 4.8.9 (including binaries for Windows and MacOS)

JavaSMT 3.6.1

Updates solver versions:

• Boolector 3.2.1-30-g95859db8
• Princess 2.13 (2020-09-18)
• SMTInterpol 2.5-732-gd208e931
• Yices2 2.6.2-396-g194350c1
• Z3 4.8.9

Improvements:

• Maven release is working again (available solvers: SMTInterpol and Princess)

JavaSMT 3.6.0

News on Solvers:

• a new solver is available: Yices 2.6.2

Licensing:

• JavaSMT is now REUSE compatible.

JavaSMT 3.5.1

Improvements and Fixes:

• improve interpolation error detection for MathSAT5
• fix simplification procedure for MathSAT5
• improve interrupt detection for Z3
• fix quantifier elimination for Z3

JavaSMT 3.5.0

This release mostly contains updated solvers,
including the new version of Z3 without support for interpolation.
There were some internal fixes and improvements.

Updates solver versions:

• CVC4 prerelease-2020-06-13-g3a1bce1b8
• Boolector 3.2.1-15-g59c9ade5
• MathSAT5 5.6.3
• OptiMathSAT 1.7.1
• Princess 2.13
• Z3 4.8.8 (info: interpolation no longer available!)

JavaSMT 3.4.0

Changes in the API:

• With the update of SMTInterpol some partially visible classes were touched.

Improvements and Fixes:

• fix for visiting uninterpreted function with CVC4
• New or updated solver versions:
  • SMTInterpol: 2.5-604-g71e72f93, including a small change in the API of SMTInterpol
• Several updates for dependencies.

JavaSMT 3.3.0

Changes in the API:

• FloatingPointManager supports more arithmetic methods, such as min, max, abs, sqrt.

Improvements and Fixes:

• More consistency checks on bitvector constants
• The Maven release contains the bindings for Princess
• New or updated solver versions:
  • Boolector 3.0.0-2019-11-11-g9d06cc0 was added (#174).
  • CVC4: 1.8-prerelease-2019-11-30-gae93e65
  • Princess: 2.12-2019-11-20
  • SMTInterpol: 2.5-533-ga4ba1513
  • other solvers were not updated since the last release

JavaSMT 3.2.0

The biggest change is the integration of the CVC4 SMT solver (CVC4 1.8-prerelease).

JavaSMT 3.1.0

This is mostly a cleanup release that contains several smaller changes and optimizations.

We included new solver versions:

• OptiMathSAT: 1.6.3
• SMTInterpol: 2.5-515-g2765bdd