Generalization Correctness

We are implementing a procedure for generalizing SMT counterexamples. In doing so we have developed a specification for what it means for a generalization to be correct and a formalization of our generalization algorithm. In proving that our algorithm satisfies our specification, we uncovered a subtle and interesting error in our generalization rules.