Sat-Based Counterexample-Guided Abstraction Refinement