Interpolation Properties and SAT-based Model Checking