Infinite-state invariant checking with IC3 and predicate abstraction