diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-15 13:45:12 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-15 18:45:12 +0000 |
| commit | 43143941e463bbe46cfb067650c64c7d10bc9a92 (patch) | |
| tree | d01447aaf6b0ece95ecc1699be4b8acaccbc003a /src | |
| parent | 56a30b7ae82b82606fe9e46e3a2c47b963e6a8e6 (diff) | |
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.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
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) { } |