projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 61aa589) | patch
[proofs] Fix open sat proof (#7509)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Fri, 5 Nov 2021 22:48:22 +0000 (19:48 -0300)
committerGitHub <noreply@github.com>
Fri, 5 Nov 2021 22:48:22 +0000 (22:48 +0000)
commit0181355bdf6b76fc550a2dca16fc0ac5e48c25ca
tree7d5643d2be7bf62beee3d6db52dba519513759b4tree
parent61aa589c4a702ee378c5b3643f4a69373da2d360commit | diff
[proofs] Fix open sat proof (#7509)

Improves how LazyCDProofChain handles cycles, which fixes a particular case triggered by the added regression. Also makes LazyCDProofChain::getProofFor more robust in that when it can't connect the requested fact it yields an assumption proof node.

Fixes cvc5/cvc5-projects#324
src/proof/lazy_proof_chain.cpp diff | blob | history
src/prop/sat_proof_manager.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2 [new file with mode: 0644] blob