Property Directed Reachability for QF_BV with mixed type atomic reasoning units

The generalization of Property Directed Reachability (PDR) for the theory QF_BV presented in [1] outperforms the original formulation if the required inductive invariant can be represented efficiently as a set of polytopes. However, many QF_BV model checking instances do not belong in this class and can be solved quickly with the original PDR algorithm. In this paper, we present a hybrid approach which uses both polytopes and Boolean cubes as atomic reasoning units combining the advantages of either homogeneous approach. We discuss theoretic properties of the presented algorithm and report experimental results demonstrating its effectiveness.