Generalization Correctness

D. Greve

14th International Workshop on the ACL2 Theorem Prover and Its Applications, May 2017

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.