Variable hiding and predicate abstraction are two popular abstraction methods to obtain simpli ed models for model checking. Although both methods have been used successfully in practice, no attempt has been made to combine them in counterexample guided abstraction re nement (CEGAR). In this paper, we propose a hybrid abstraction method that allows both visible variables and predicates to take advantages of their relative strengths. We use re nement based on weakest preconditions to add new predicates, and under certain conditions trade in the predicates for visible variables in the abstract model. We also present heuristics for improving the overall performance, based on static analysis to identify useful candidates for visible variables, and use of lazy constraints to nd more effective unsatis able cores for re nement. We have implemented the proposed hybrid CEGAR procedure. Our experiments on public benchmarks show that the new abstraction method frequently outperforms the better of the two existing abstraction methods.