Added many assertions. PDR now fails if inductive generalization, unsat core, and block in future are all turned off