Inductive generalization with unsat cores

Still buggy, will throw assertion failures