Golem


Golem is a new CHC solver still under active development. It can solve systems of linear clauses with Linear Real or Integer Arithmetic as the background theory and it is able to provide witnesses for both satisfiable and unsatisfiable systems.
Its current reasoning engine is a re-implementation of the Impact algorithm and thus falls into the category of interpolation-based model-checking approaches.


Golem is implemented in C++ and built on top of the interpolating SMT solver OpenSMT which is used for both satisfiability solving and interpolation.
Golem finished second in LIA-Lin and LRA-TS tracks of the last CHC competition
CHC competition presentation is available Here
The current implementation of Golem lives as a fork of OpenSMT's repository at https://github.com/blishko/opensmt/tree/golem