minor changes to string constant names to avoid confusion in other
boogie tools