Automated Abstraction by Incremental Refinement in Interpolant-based Model Checking