v0.8.1

This is a bugfix release for handling auxiliary variables in engines working on transition systems. This bug was introduced in 0.7.0.
The internal validator has been strengthened to detect such regressions.

v0.8.0

Notable changes:

• Fixed bug in printing 0-ary predicates in models
• Fixed model format to conform to SMT-LIB
• Fixed bug in preprocessing in the presence of array
• Added a new backend engine based on forward symbolic execution
• Improved automatic detection of background theory
• Updated Alethe proofs to conform to latest Alethe specification

v0.7.1

This release fixes a regression in 0.7.0 in KIND and TPA engines related to handling auxiliary variables

v0.7.0

This release upgrades the version of OpenSMT used, and also bumps C++ standard to C++20.
Some notable changes are

• Very preliminary experimental support for arrays, only available with engines bmc and kind
• Experimental extension of kind to run on general linear CHC systems (not only transition systems).
• Fixed witness printing in case multiple engines run in parallel.

v0.6.5

Compared to the previous release, this one includes more powerful preprocessing and performance optimization in PDKIND engine.

v0.6.4

Compared to 0.6.3, this is a small release focused on fixes in the preprocessing.

v0.6.3

New engine

Golem now has a new engine based on Dual approximated reachability, available with --engine dar.

Engine improvements

• Performance of IMC engine has been improved.
• Performance of predicate abstraction engine has been improved.
• Implementation of TPA for DAG of transition systems have been simplified in line with the published pseudocode.
• TPA now handles nested loops in a more structural way.

Miscellaneous

• Alethe proofs are now a bit more compact.

v0.6.2

Small fixes

• Fix the version that is printed using --version flag
• Remove unnecessary empty lines from the legacy proof format

v0.6.1

Small bugfixes

• Reject more inputs outside of supported fragment (instead of incorrect internalization leading to wrong answer)
• Ensure correct order of premises in the UNSAT proofs

v0.6.0

Main changes

• Update OpenSMT to 2.7.0
• Add PDKIND engine (@stepanhen)
• Add simple prototype engine for Predicate Abstraction

Various improvements

• Improve performance of Alethe proof generation
• Improve performance of BMC engine on general linear system (now uses dedicated algorithm instead of transformation to transition system
• Improve performance of IMC engine
• Printing negative numbers in models is now SMT-LIB2 compliant
• Input outside of Horn fragment is gracefully rejected