Flexible Interpolation for Efficient Model Checking