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's repository can be found at GitHub: https://github.com/usi-verification-and-security/golem

Golem finished second in LIA-Lin and LRA-TS tracks of the last CHC competition. 

CHC competition presentation is available Here