diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-02-03 12:11:26 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-03 09:11:26 -0600 |
| commit | a6c122da21b3d5b9c37d9ec670dec766eaff7001 (patch) | |
| tree | b5586c3fcc7dd18a6304464cb5a5611bb2709a1c /src/options | |
| parent | d97cee1a7c1a688d1ad9c748247bd9da1d86973f (diff) | |
[proof-new] Fix MACRO_RESOLUTION expansion for singleton clause corner case (#5850)
Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which the resulting clause from crowding literal elimination is a singleton. This commit makes the expansion code robust to that and adds an example of a problematic benchmark as a regression.
Also improves a bit tracing and some comments.
Diffstat (limited to 'src/options')
0 files changed, 0 insertions, 0 deletions