Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases