Use unsat cores to find out which quantifier instances are used

[zhengyao-lin]

(This is not an issue but more of a question)

Hello! I'm trying to modify Z3 to indicate which instances after QI are used to prove unsat (but not all instances ever created).

I'm not familiar with the Z3 code base, but one way I tried was to mark each instance with a name (similar to how one would add a :named attribute to an assertion), and then I was hoping that these names get used during the process of producing the unsat core.

Right now I figured out how to create a literal to represent an instance (in qi_queue::instantiate(entry & ent)), but then I'm not sure how to ask the SAT solver to consider these literals. I tried updating context::m_literal2assumption and context::m_assumptions like how the initial named assertions are processed, but it didn't seem to work.

Is this a feasible approach? If so, could you please suggest how to use these new literals for the unsat core?
If not, is there another way to implement this functionality of producing unsat cores that include QI instances?

Thank you!

[NikolajBjorner]

Can you use the option solver.instantiations2console=true?
It isn't used by external users so far, so could need some revisions.
Overall, I will consolidate some of this using a more generic proof logging mechanism, but for now, the instantiatinos2console is intended to show instances in a format that can be inspected.