Fix context for proofs of instantiations (#6890)

Caught by a regression on proof-new, where an instantiation was the symmetric equality of an instantiation on a previous call to check-sat. Proofs of instantiation should be user-context dependent.

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index f4cd8cb6927ce859b8dfce5693ce97deaf6bd5c2..268d1371f59fcf6fe5b8b8252ed5e867a069e3b8 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -56,7 +56,9 @@ Instantiate::Instantiate(QuantifiersState& qs,
       d_pnm(pnm),
       d_insts(qs.getUserContext()),
       d_c_inst_match_trie_dom(qs.getUserContext()),
-      d_pfInst(pnm ? new CDProof(pnm) : nullptr)
+      d_pfInst(
+          pnm ? new CDProof(pnm, qs.getUserContext(), "Instantiate::pfInst")
+              : nullptr)
 {
 }