Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop