Efficient Weighted Model Integration via SMT-Based Predicate Abstraction