Skip to content

Parser silently overflows on big variable numbers #3

@lammich

Description

@lammich

BUG. Allows SAT formulas being certified as UNSAT.

Although it is documented that variable numbers must be less than 2^31, drat-trim silently overflows on big variable numbers, erroneously identifying different variables.

Suggestion to fix: Terminate with error message, instead of silently overflowing.

f4.zip

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions