After many years of successful development of new approaches for software verification, there is a need to consolidate the knowledge about the different abstract domains and algorithms. Several of the most widely used approaches for software model checking are based on solving first-order-logic formulas over predicates using SMT solvers, e.g., predicate abstraction, bounded model checking, k-induction, and lazy abstraction with interpolants. We define a configurable framework for predicate-based analyses that allows expressing each of these approaches and is based on CPAchecker's core concept, configurable program analysis. This unifying framework highlights the differences between the approaches, producing new insights, and facilitates research of further algorithms and their combinations. To pinpoint both the similarities and differences between the approaches, we exercise the approaches on a running example. Finally, we use the implementation of our unifying framework for predicate analysis in CPAchecker to perform an experimental study. We evaluate the effect of varying the SMT solver and the way program semantics are encoded in formulas across several verification algorithms and find that these technical choices can significantly influence the results of experimental studies of verification approaches. This is valuable information for both researchers who study verification approaches as well as for users who apply them in practice and motivates upcoming changes in CPAchecker's default configurations.