diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-09 13:49:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-09 15:49:10 -0500 |
commit | c74e9c8ba946387616345b70d63028896a0022c2 (patch) | |
tree | a7446c7a7682845073390801b4f4acc498baccce /proofs | |
parent | 3740873b8b1ac7e1f2c203b26de6dd1a0ef73f43 (diff) |
Make registration of unit clauses more robust (#3965)
Fixes #3959. It can happen that we generate a lemma that results in a
unit clause that matches a unit clause that was added as an input.
However, we are asserting that a unit clause can only be registered as
either one of them. This commit fixes the issue by only registering a
unit clause from a lemma if it is not already satisfied. I chose this
fix because the existing code doesn't seem to do anything (in terms of
solving) for the case where we have a unit clause that is already
satisfied because of an input unit clause.
Diffstat (limited to 'proofs')
0 files changed, 0 insertions, 0 deletions