  Modern program verifiers use logic-based encodings of the verification
problem that are discharged by a back end reasoning engine. However, instances
of such encodings for large programs can quickly overwhelm these back end
solvers. Hence, we need techniques to make the solving process scale to large
systems, such as partitioning (divide-and-conquer) and abstraction.
  In recent work, we showed how decomposing the formula encoding of a
termination analysis can significantly increase efficiency. The analysis
generates a sequence of logical formulas with existentially quantified
predicates that are solved by a synthesis-based program analysis engine.
However, decomposition introduces abstractions in addition to those required
for finding the unknown predicates in the formula, and can hence deteriorate
precision. We discuss the challenges associated with such decompositions and
their interdependencies with the solving process.
