Precise and automatic verification of container-manipulating programs