projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f1c384d) | patch
[proof-new] Fix handling of removable clauses in proof cnf stream (#5961)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Tue, 23 Feb 2021 14:59:32 +0000 (11:59 -0300)
committerGitHub <noreply@github.com>
Tue, 23 Feb 2021 14:59:32 +0000 (11:59 -0300)
commitc2311f97441befbf10e80ab597455b3ab8ccc10c
tree17bfbc7e3020aadb9bf14d3097b02bbd56934f7btree
parentf1c384dff82bffa56b9cf9ba18ec1f35aa529b12commit | diff
[proof-new] Fix handling of removable clauses in proof cnf stream (#5961)

Previously the removable information was not being communicated from the proof cnf stream to the cnf stream, which is the one that actually uses this when asserting clauses into the SAT solver. This commit fixes this by having the proof cnf stream directly use the cnf stream d_removable attribute.
src/prop/proof_cnf_stream.cpp diff | blob | history
src/prop/proof_cnf_stream.h diff | blob | history