Computing Predicate Abstractions by Integrating BDDs and SMT Solvers