diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-03-03 21:24:43 -0800 |
|---|---|---|
| committer | Alex Ozdemir <aozdemir@hmc.edu> | 2019-03-03 21:24:43 -0800 |
| commit | e4f3ffc1a2c8305b5e56fabc01a91e85d20aab45 (patch) | |
| tree | a3030b5cfe77988935c383969bcc2fbcdd8183c3 /src/main/driver_unified.cpp | |
| parent | 0887a032badd631fa5be2eac83cadfaccff893d1 (diff) | |
Another DRAT/LRAT compatibility bug
There was a problem in which if a DRAT proof failed to meet the
specifified requirements in the final addition of the empty clause.
Specifically, the empty clause would not be an AT, and then resolution
search would trigger and fail because the empty clause can't resolve
with stuff. Now we just return false, causing operational DRAT checking
to start.
Diffstat (limited to 'src/main/driver_unified.cpp')
0 files changed, 0 insertions, 0 deletions