Binary format not correcty detected

[msoos]

./drat-trim fuzzTest_33.cnf fuzzTest_33.cnf-drat

gives:

c parsing input formula with 53 variables and 116 clauses
c ERROR: comment longer than 1024 characters: a2Rf\Z`bdT

By forcing the binary mode (only possible via hacking the code...):

../../build/tests/drat-trim/drat-trim  out/fuzzTest_33.cnf out/fuzzTest_33.cnf-drat
c parsing input formula with 53 variables and 116 clauses
c finished parsing, read 1203958 bytes from proof file
c detected empty clause; start verification via backward checking
c 116 of 116 clauses in core                            
c 44292 of 55206 lemmas in core using 740218 resolution steps
c 0 RAT lemmas in core; 11329 redundant literals in core lemmas
s VERIFIED
c verification time: 1.386 seconds

This was found using an extensive fuzzer that I built to fuzz CMS. Unfortunately/fortunately, it found a bug in DRAT instead :S

drat.zip

Can we have a force-binary mode please? Also, what is the bug about? I can't seem to wrap my head around it. The detector seems to be wrong. The hexdump seems OK and starts with the right character ("a"):

hexdump -C out/fuzzTest_33.cnf-drat | head
00000000  61 32 52 66 5c 5a 60 62  64 54 02 00 61 08 49 6a  |a2Rf\Z`bdT..a.Ij|
00000010  1a 56 68 62 5a 3d 00 61  49 3d 6a 68 1a 56 5a 62  |.VhbZ=.aI=jh.VZb|
00000020  64 54 02 00 61 10 52 5a  54 62 64 60 02 66 6a 68  |dT..a.RZTbd`.fjh|
00000030  56 0b 58 5c 00 61 52 54  68 5c 6a 56 02 5a 58 62  |V.X\.aRTh\jV.ZXb|
00000040  64 60 66 5e 00 61 30 1a  56 68 49 41 6a 00 61 1a  |d`f^.a0.VhIAj.a.|
00000050  05 41 6a 56 49 62 64 54  68 00 61 05 41 68 6a 56  |.AjVIbdTh.a.AhjV|
00000060  49 62 64 54 02 5e 16 00  61 41 16 68 5e 6a 02 56  |IbdT.^..aA.h^j.V|
00000070  54 49 64 62 5a 53 00 61  18 40 02 54 5a 64 62 00  |TIdbZS.a.@.TZdb.|
00000080  61 2a 2e 53 5a 16 40 5e  02 54 00 61 3c 54 5e 02  |a*.SZ.@^.T.a<T^.|
00000090  53 5a 62 64 68 6a 56 66  58 5c 00 61 1a 41 68 56  |SZbdhjVfX\.a.AhV|

[msoos]

The fuzzer found multiple examples, I'm just going to put the hexdump here of the other 2:

hexdump -C out/fuzzTest_36.cnf-drat | head
00000000  61 4c 4e 35 5a 20 66 4a  5e 64 1b 54 56 0b 00 61  |aLN5Z fJ^d.TV..a|
00000010  4e 50 54 0b 1b 64 5e 6a  35 20 5a 4a 56 66 00 61  |NPT..d^j5 ZJVf.a|
00000020  31 50 35 20 5a 4a 66 0b  56 00 61 08 12 33 56 4a  |1P5 ZJf.V.a..3VJ|
00000030  0b 50 00 61 12 33 56 0b  50 4a 5a 45 6a 40 00 61  |.P.a.3V.PJZEj@.a|
00000040  3b 40 50 6a 4a 45 5a 00  61 24 45 5a 6a 4a 50 0b  |;@PjJEZ.a$EZjJP.|
00000050  20 66 56 35 00 61 50 54  56 0b 35 4a 6a 5a 20 5e  | fV5.aPTV.5JjZ ^|
00000060  64 1b 66 00 61 32 09 6a  5a 45 20 35 00 61 3b 09  |d.f.a2.jZE 5.a;.|
00000070  42 35 66 20 39 6a 4a 45  5a 00 61 09 45 5a 4a 6a  |B5f 9jJEZ.a.EZJj|
00000080  66 35 42 20 2c 00 61 54  56 35 20 5a 4a 6a 0b 66  |f5B ,.aTV5 ZJj.f|
00000090  5e 1b 64 00 61 09 07 56  66 0b 4a 48 5a 33 45 55  |^.d.a..Vf.JHZ3EU|

hexdump -C out/fuzzTest_35.cnf-drat | head
00000000  61 20 46 5e 6a 66 43 5c  4e 50 54 64 52 00 61 2b  |a F^jfC\NPTdR.a+|
00000010  46 54 64 50 4e 66 5c 58  43 48 6a 3c 52 00 61 46  |FTdPNf\XCHj<R.aF|
00000020  48 64 50 4e 5c 43 6a 52  54 58 66 5e 4a 4c 62 00  |HdPN\CjRTXf^JLb.|
00000030  61 2b 16 60 54 64 50 4e  66 5c 58 43 48 6a 3c 52  |a+.`TdPNf\XCHj<R|
00000040  00 61 23 48 54 64 50 4e  5c 43 6a 52 60 58 66 5e  |.a#HTdPN\CjR`Xf^|
00000050  02 4a 00 61 15 48 60 4a  02 58 66 5e 52 6a 43 5c  |.J.a.H`J.Xf^RjC\|
00000060  4e 50 64 20 54 00 61 31  48 60 4a 02 58 66 5e 54  |NPd T.a1H`J.Xf^T|
00000070  52 20 6a 64 43 50 5c 4e  00 61 48 4a 54 64 50 4e  |R jdCP\N.aHJTdPN|
00000080  5c 02 43 60 6a 52 5e 58  66 62 4c 00 61 4a 4c 02  |\.C`jR^XfbL.aJL.|
00000090  60 62 54 58 66 5e 64 52  50 6a 4e 43 5c 00 61 4c  |`bTXf^dRPjNC\.aL|

Please fix :)

[marijnheule]

This is fixed now.