Adjusted Verification Rules for Loops Are More Complete and Give Better Diagnostics for Less