v2.8.0

API changes:

• Enclosed the whole project into opensmt namespace.
• Using also directory names when including files.
• Adapted parts of the API of MainSolver to the SMT-LIB 2.6 terminology that uses "assertion stack".

Bug fixes:

• Named terms: do not report error when re-introducing a named term with an already popped name.
• Do not reverse the arguments of XOR terms.

New features:

• Support ":minimal-unsat-cores" option - naive implementation of subset-minimal unsat cores.
• Support ":print-cores-full" option - make the unsat cores strictly agnostic to the ":named" terms.

Build:

• Switch to C++20.
• Bumped minimal CMake version to 3.14.

v2.7.0

Bug fixes:

• Fix unsoundness in incremental solving involving theory combination (introduced in 2.6.0).
• Fix unsoundness in handling nested arrays.
• Fix bug in one of the constructors of FastRational.

New features:

• Experimental support for unsat cores.

v2.6.0

Notable changes since last release.

• Added support for command (set-logic ALL).
• Added helper script to build OpenSMT with a single make command (this still invokes CMake under the hood).
• Performance improvement in preprocessing for incremental solving. Helpful for use case with a lot of simple queries.
• Dropped support for readline library. Line-editing capabilities are still available with linking to libedit.
• OpenSMT is now supported in JavaSMT.

v2.5.2

This is a patch release contains small updates required for changes in CircleCI builds.

Additionally, some corner cases have been fixed for div and mod operators and an API method for convenient creation of array variables has been added.

v2.5.1

This release fixes a couple of issues in the front end. Specifically, it fixes the response to the get-value command and processing of define-fun commands where previously OpenSMT incorrectly reported name clashes for parameters in some cases.
Additionally, a problem for benchmarks with theory combination where sometimes OpenSMT would enter infinite cycle in a preprocessing has been fixed.

v2.5.0

This release fixes a bug in our array solver and extends OpenSMT's supported theories with the combination of arrays and arithmetic (and uninterpreted functions).
Additionally, Lookahead solver in OpenSMT now supports incremental solving and interpolation, and a new heuristic ("picky") has been added. This heuristic restricts the Lookahead search to a constant number of variables, and it tries the best ones according to CDCL score.

v2.4.3

This is a bug fix release for unsoundness in solving QF_UFLRA and QF_UFLIA formulas.
There was a bug in our approach to theory combination that slipped into the last release (v2.4.2).

v2.4.2

This release contains a fix for a dependency on the order of initialization of global objects that caused crashes in array solver on new MacOS with M2 chip.
Additionally it contains a bug fix and performance improvement for the parallel version of OpenSMT and a performance improvement for arithmetic logics based on better substitution analysis.

v2.4.1

This is a patch release that fixes a use of uninitialized value in 2.4.0.

v2.4.0

This release contains performance improvements thanks to the changes in the core SAT solver contributed by @msoos.

It also contains a new way to use OpenSMT in parallel mode implemented by @MasoudAsadzade.
OpenSMT needs to be built using CMake option -DPARALLEL:BOOL=ON. This is done automatically when using our parallel framework SMTS.

Finally, this release adds support for the SMT-LIB logic QF_AX. Combination of arrays with integer arithmetic should follow soon!