projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 56a30b7) | patch
Fix context for proofs of instantiations (#6890)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 15 Jul 2021 18:45:12 +0000 (13:45 -0500)
committerGitHub <noreply@github.com>
Thu, 15 Jul 2021 18:45:12 +0000 (18:45 +0000)
commit43143941e463bbe46cfb067650c64c7d10bc9a92
treed01447aaf6b0ece95ecc1699be4b8acaccbc003atree
parent56a30b7ae82b82606fe9e46e3a2c47b963e6a8e6commit | 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.
src/theory/quantifiers/instantiate.cpp diff | blob | history