projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5d0bc27) | patch
Make CAD proofs user context dependent (#7466)
authorGereon Kremer <nafur42@gmail.com>
Fri, 22 Oct 2021 18:08:33 +0000 (11:08 -0700)
committerGitHub <noreply@github.com>
Fri, 22 Oct 2021 18:08:33 +0000 (18:08 +0000)
commit0b7b6fb608a897bf50861ce5a4c25e74c9245f01
treed1c2ab687f4c40a67a3efce292d48ea5d86050d9tree
parent5d0bc27685611a9ee738507a45f5b68b6da42d8acommit | diff
Make CAD proofs user context dependent (#7466)

Given that arithmetic lemmas can survive the current (sat) context by being buffered in the inference manager, their proofs need to do as well. This PR changes the CAD proofs to be user context dependent.

Fixes cvc5/cvc5-projects#315.
src/theory/arith/nl/cad/cdcac.cpp diff | blob | history
test/regress/regress0/arith/issue5219-conflict-rewrite.smt2 diff | blob | history