Effective word-level interpolation for software verification