diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-03 17:30:41 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-03 17:30:41 -0700 |
| commit | fee2021bb7419630853cbd0b20afa1af5e2eb1e9 (patch) | |
| tree | e4d6ff6757bfffb11cb1f101cf1fb6d1b16f784f /test/regress | |
| parent | 5248998baff098d6b28a80f7bd2f286dfa942148 (diff) | |
[BVMiniSat] Avoid duplicates in conflicts (#1745)
If analyzeFinal() in BVMiniSat was called with a literal that also
occurred in the trail, it could happen that the set of assumptions that
led to the assignment of `p` contained `p` twice.
BitVectorProof::endBVConflict would then register that conflict with the
duplicate literal but at the same time compute a conflict expression
with the duplicate removed. LFSCSatProof::printAssumptionsResolution
would then output two resolutions for the same literal, which made the
simplify_clause side condition fail because it couldn't find the literal
in the clause anymore after the first removal.
The fix simply avoid adding `p` to the set of assumptions if it is found
in the trail. In this situation, `p` is guaranteed to be in the set of
assumptions already because it has been added at the beginning of
analyzeFinal(). This issue originally came up in PR #1384. With this fix
the regression tests pass in #1384.
Diffstat (limited to 'test/regress')
0 files changed, 0 insertions, 0 deletions