Segfault

[msoos]

Hi,

The system died on the first proof I gave it, gave a segfault, which should never happen as it should correctly validate input:

$ rupee -binary out dr
c Parsing CNF instance out
c Parsing DRAT proof dr
c Checking DRAT proof
s REJECTED
Segmentation fault (core dumped)

Tarball attached that contain both out and dr. stuff.tar.gz

drat-trim on the same input:

$ drat-trim out dr
c turning on binary mode checking
c parsing input formula with 2454 variables and 8300 clauses
c finished parsing, read 1523364 bytes from proof file
c detected empty clause; start verification via backward checking
c 3989 of 8300 clauses in core                            
c 16385 of 27825 lemmas in core using 1335562 resolution steps
c 0 RAT lemmas in core; 15530 redundant literals in core lemmas
s VERIFIED
c verification time: 1.128 seconds

This is literally the first input I gave to this checker.

[arpj-rebola]

There was a bug on the procedure reintroducing literals after unit deletion. Fixed now, works for your instance with rupee out dr -full-deletion -binary

[msoos]

Thanks a lot!

Mate