Boosting the role of inductive invariants in model checking