Tighter Integration of BDD and SMT for Predicate Abstraction