diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-02-02 11:17:33 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-02 11:17:33 -0300 |
| commit | 95add26e5210e53e03c55ee313279b87cc3d5660 (patch) | |
| tree | b5032ea99a12eac9c5facf66ac53fdb8c25de02d /src/theory | |
| parent | c48548ea68b6241bee2cb9393ef2710c5803fb06 (diff) | |
[proof-new] Fix bug in expansion of MACRO_RESOLUTION (#5845)
Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which a crowding literal occurs in an OR node that represents a single-literal clause subsequent to the last clause that includes the crowding literal. This was leading to the clause that eliminates the crowding literal not being found. The commit fixes this issue by excluding single-literal clauses from those that can introduce crowding literals (which was already marked as necessary but not properly enforced).
Diffstat (limited to 'src/theory')
0 files changed, 0 insertions, 0 deletions