The Engineering of a Model Checker: The Gnu i-Protocol Case Study Revisited