  In this paper we revisit the topic of generalizing proof obligations in
bit-level Property Directed Reachability (PDR). We provide a comprehensive
study which (1) determines the complexity of the problem, (2) thoroughly
analyzes limitations of existing methods, (3) introduces approaches to proof
obligation generalization that have never been used in the context of PDR, (4)
compares the strengths of different methods from a theoretical point of view,
and (5) intensively evaluates the methods on various benchmarks from hardware
model checking as well as from AI planning.
