v2.9.2

New features:

• Supporting unsat-core options in the command line executable.

v2.9.1

Bug fixes:

• Fixed assertion violation for LIA.
• Fixed handling of split clauses.

Other:

• Optimized and sanitized LA substitutions.
• Unified functions for polyToPTRef and back.

v2.9.0

API changes:

• Refactored number-related source files into a separate directory.
• Divided InterpolationUtils into multiple headers.
• MainSolver: deprecated non-const getTermNames, replaced by tryAddNamedAssertion/tryAddTermNameFor.
• Made some functions as const in Logic and ArithLogic.

Documentation:

• Reintroduced help message.

New features:

• Implemented simple extensions of a Model.
• Support printing the version including commits.

Other:

• Refactored and simplified handling of bounds in LASolver.

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).