Towards Scalable Fully Automatic Program Verification