From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 15 Jul 2021 18:45:12 +0000 (-0500)
Subject: Fix context for proofs of instantiations (#6890)
X-Git-Tag: cvc5-1.0.0~1476
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=43143941e463bbe46cfb067650c64c7d10bc9a92;p=cvc5.git

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 f4cd8cb69..268d1371f 100644
--- 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)
 {
 }