diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-10 23:25:21 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-10 23:25:21 -0700 |
| commit | edcc81b08b4d6c67da81b7ba2fcefbab3286f02c (patch) | |
| tree | 2ed2aabf8763b96228d4629056a2d04208c8eab5 /src/theory/quantifiers | |
| parent | ad2fc7c63e8f9d91ff0b750207fdae5fd029134b (diff) | |
Set assertion in `CnfStream::ensureLiteral()` (#3927)
Fixes #3814. `CnfProof` has a stack of assertions that are being
converted to clauses. `CnfStream::ensureLiteral()` can result in clauses
being added to the SAT solver. When adding a clause, we require an
assertion that can be associated with the clause
(https://github.com/CVC4/CVC4/blob/ba6ade0fc3f4cd339885652bb9bf5c87113c498d/src/prop/minisat/core/Solver.cc#L471-L476).
However, in the issue that was reported, the stack was empty, resulting
in an assertion failure. This commit fixes the issue by setting the
current assertion to be the null node when a literal is being ensured
(and changing the proof code to update the assertion associated with a
literal if it is currently null). This should be ok since the clauses
are not inputs or lemmas (if they are, the assertion associated with the
clause will be updated).
Diffstat (limited to 'src/theory/quantifiers')
0 files changed, 0 insertions, 0 deletions