projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4a84ee3) | patch
[unsat-cores] [sat-proof] Fix open proofs due to theory lemmas (#8371)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Thu, 24 Mar 2022 15:32:42 +0000 (12:32 -0300)
committerGitHub <noreply@github.com>
Thu, 24 Mar 2022 15:32:42 +0000 (15:32 +0000)
commit2044c5b87f2b7fde24c3a57a626e903663f34e15
tree455dd10ea411d5bd7bb557f53432f496de241132tree
parent4a84ee32687d84ff18835c23196086f1ef1ba3aacommit | diff
[unsat-cores] [sat-proof] Fix open proofs due to theory lemmas (#8371)

Previously when producing sat proofs for unsat cores (no theory proofs) theory lemmas were becoming open leafs in the final proof, breaking the invariant that only inputs should be so. This commit guards against this by justifying these lemmas with a THEORY_LEMMA step.

Fixes cvc5/cvc5-projects#468
src/prop/proof_cnf_stream.cpp diff | blob | history
src/prop/prop_engine.cpp diff | blob | history
src/prop/prop_engine.h diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/proofs/proj-issue468-mkScope.smt2 [new file with mode: 0644] blob