From 43143941e463bbe46cfb067650c64c7d10bc9a92 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 15 Jul 2021 13:45:12 -0500 Subject: [PATCH] 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. --- src/theory/quantifiers/instantiate.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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) { } -- 2.30.2