Improved termination analysis so that daikon generated specifications won't have...