Interpolation with Guided Refinement: revisiting incrementality in SAT-based Unbounded Model Checking