diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-02-23 11:59:32 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-23 11:59:32 -0300 |
| commit | c2311f97441befbf10e80ab597455b3ab8ccc10c (patch) | |
| tree | 17bfbc7e3020aadb9bf14d3097b02bbd56934f7b /src/prop/proof_cnf_stream.h | |
| parent | f1c384dff82bffa56b9cf9ba18ec1f35aa529b12 (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.
Diffstat (limited to 'src/prop/proof_cnf_stream.h')
| -rw-r--r-- | src/prop/proof_cnf_stream.h | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h index 1f3d043b8..12beaf6eb 100644 --- a/src/prop/proof_cnf_stream.h +++ b/src/prop/proof_cnf_stream.h @@ -151,13 +151,6 @@ class ProofCnfStream : public ProofGenerator * above normalizations on all added clauses. */ void normalizeAndRegister(TNode clauseNode); - /** - * Are we asserting a removable clause (true) or a permanent clause (false). - * This is set at the beginning of convertAndAssert so that it doesn't need to - * be passed on over the stack. Only pure clauses can be asserted as - * removable. - */ - bool d_removable; /** Reference to the underlying cnf stream. */ CnfStream& d_cnfStream; /** The proof manager of underlying SAT solver associated with this stream. */ |