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

v0.5.0

Main changes

• Update OpenSMT to v2.6.0
• Production of unsatisfiability proofs in Alethe format (--proof-format=alethe)
• More aggressive simplifications in preprocessing
• Preliminary support for model computation (invariants) in TPA engine for general linear systems
• Various small bug fixes and performance improvements.

Contributors

@blishko @BritikovKI @m4mbo

v0.4.3

Changes in the current release

• Fix bug in backtranslating proofs in one of the preprocessing passes
• Add new default preprocessing pass
• Implement transformation of linear CHC systems into transition systems (enabled in BMC and IMC)
• Better invariant detection in TPA
• Performance improvements in Spacer

v0.4.2

This is a simple bugfix release which fixes a problem in printing models where the names of the predicates need to be SMT-LIB-quoted.
Additionally, a new option --version has been added to print the version of the binary.

v0.4.1

This patch contains a fix in witness backtranslation and a small fix for printing satisfiability witnesses.
Additionally, this introduces an experimental feature which allows Golem to run several engines in parallel, each as a separate process.

v0.4.0

This release extends the set of supported linear systems in TPA engine from chain of transition system to a DAG of transition systems.
Also, TPA engine will now also handle non-recursive systems of Horn clauses.

Additionally, with this release Golem now uses the latest release of OpenSMT: v2.5.0

v0.3.2

This release fixes a bug in the TPA engine in the analysis of chains of transition systems (analysis of a single transition system is not affected by the problem).

v0.3.1

This release contains some performance improvement, especially in Spacer engine.
The algorithm now avoids some redundant work with the solver and also benefits from improved preprocessing.
Additionally, a minor bug in backtranslation of witnesses has been fixed, and a support for backtranslation of UNSAT proofs has been added for the transformation passes that contract nodes.

v0.3.0

This release adds new engine to the supporting backend: IMC, the original interpolation-based model-checking algorithm from McMillan.
It was contributed by @BritikovKI.

Additionally, with this release, the Spacer engine now also produces proofs of unsatisfiability.
The output format of the unsatisfiability proof has been changed and now follows more closely the output format as printed by Eldarica.

v0.2.0

This release updates the dependency OpenSMT to version 2.4.3.
It also contains a small improvement to Spacer engine.