term-comp-25

This is a special release corresponding to the entry for TERM-COMP '25.

v0.9.0

This release adds basic experimental support for termination problems.
Specifically, Golem can now take as input termination problems in the ARI format, specifically the Integer Transition Systems from TERM-COMP.

Currently, Golem can prove non-termination by discovering a reachable lasso in the transition system.

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