  Constrained Horn Clauses (CHCs) have conventionally been used as a low-level
representation in formal verification. Most existing solvers use a diverse set
of specialized techniques, including direct state space traversal or
under-approximating abstraction, necessitating purpose-built complex
algorithms. Other solvers successfully simplified the verification workflow by
translating the problem to inputs for other verification tasks, leveraging the
strengths of existing algorithms. One such approach transforms the CHC problem
into a recursive program roughly emulating a top-down solver for the deduction
task; and verifying the reachability of a safety violation specified as a
control location. We propose an alternative bottom-up approach for linear CHCs,
and evaluate the two options in the open-source model checking framework THETA
on both synthetic and industrial examples. We find that there is a more than
twofold increase in the number of solved tasks when the novel bottom-up
approach is used in the verification workflow, in contrast with the top-down
technique.
