This paper presents the Eldarica version 2 model checker.  Over the
  last years we have been developing and maintaining Eldarica as a
  state-of-the-art solver for Horn clauses over integer arithmetic.
  In the version 2, we have extended the solver to support also
  algebraic data types and bit-vectors, theories that are commonly
  applied in verification, but currently unsupported by most Horn
  solvers. This paper describes the high-level structure of the tool
  and the interface that it provides to other applications.  We also
  report on an evaluation of the tool.  While some of the techniques
  in Eldarica have been documented in research papers over the last
  years, this is the first tool paper describing Eldarica in its
  entirety.