  We address the problem of checking the satisfiability of a set of constrained
Horn clauses (CHCs) possibly including more than one query. We propose a
transformation technique that takes as input a set of CHCs, including a set of
queries, and returns as output a new set of CHCs, such that the transformed
CHCs are satisfiable if and only if so are the original ones, and the
transformed CHCs incorporate in each new query suitable information coming from
the other ones so that the CHC satisfiability algorithm is able to exploit the
relationships among all queries. We show that our proposed technique is
effective on a non trivial benchmark of sets of CHCs that encode many
verification problems for programs manipulating algebraic data types such as
lists and trees.
