projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c92b9fb) | patch
Fix a subtle issue with double negations in coverings proof (#7967)
authorGereon Kremer <gkremer@stanford.edu>
Wed, 19 Jan 2022 22:36:08 +0000 (14:36 -0800)
committerGitHub <noreply@github.com>
Wed, 19 Jan 2022 22:36:08 +0000 (22:36 +0000)
commit8d9d3f84a5036a0254b00e99ebe00b5fad85b14b
treed2f9daa38bb1b93ee5879255a041695d0306abdetree
parentc92b9fbd07d1db4641c3c49fc5dd8e98be25f3e6commit | diff
Fix a subtle issue with double negations in coverings proof (#7967)

When the coverings solver finds a conflict that consists only of a single negated assertion, the way we constructed the lemma would silently drop the double negation. While this is not a problem by itself, the generated proof is out of sync then.
This PR makes sure the double negation stays in place and is only removed by rewriting in the core lemma processing.
Fixes cvc5/cvc5-projects#430.
src/theory/arith/nl/cad_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/proofs/proj-issue430-coverings-double-negation.smt2 [new file with mode: 0644] blob