marijnheule/drat-trim

Issues

• Comments not properly ignored in the INPUT file

  #39 opened 8 months ago by sambuss
  0

• Validating part of the proof for both sat and unsat

  #38 opened 8 months ago by summer-yf
  0

• ignore parsing comments in binary mode

  #16 opened 6 years ago by NikolajBjorner
  4

• Forward checking with '-S' on satisfiable formulas fails.

  #35 opened 2 years ago by arminbiere
  1

• ASCII output despite -C

  #34 opened 2 years ago by lammich
  0

• Buffer overflow on trivial unsat formula

  #6 opened 2 years ago by lammich
  2

• Invalid read of memory

  #18 opened 2 years ago by msoos
  1

• lrat-check: Fails to verify large lrat files

  #23 opened 2 years ago by marchartung
  1

• Binary format not correcty detected

  #13 opened 2 years ago by msoos
  2

• No effective self-checking

  #10 opened 2 years ago by msoos
  0

• No build pipeline

  #9 opened 2 years ago by msoos
  1

• [lrat-check] CNF with two clauses causes assertion failure

  #20 opened 2 years ago by digama0
  1

• Trace check file contains clauses not in the original proof

  #7 opened 2 years ago by hgvk94
  1

• No testing at all

  #8 opened 2 years ago by msoos
  1

• Detecting and deleting duplicate literals causes coredump

  #5 opened 2 years ago by lammich
  3

• Assertion fails in some instances

  #25 opened 2 years ago by arpj-rebola
  4

• A small issue

  #30 opened 2 years ago by DennisYurichev
  3

• lrat-check accepts empty clause with empty proof

  #31 opened 2 years ago by RandomActsOfGrammar
  1

• [lrat-check] Trivial CNF causes infinite loop

  #21 opened 2 years ago by digama0
  1

• [lrat-check] Fails to ignore comments in cnf files

  #22 opened 2 years ago by digama0
  1

• Realloc not guarded against memory failure

  #19 opened 2 years ago by msoos
  2

• drat_trim.c int overflow

  #33 opened 2 years ago by xyz2606
  1

• How to convert DRAT/DRUP to LRAT?

  #29 opened 3 years ago by DennisYurichev
  8

• handle compressed files?

  #27 opened 3 years ago by c-cube
  0

• C++ API

  #14 opened 6 years ago by alex-ozdemir
  0

• Using "false" as a variable name is not recommended

  #11 opened 7 years ago by msoos
  2

• The system does not deal with zipped CNF files

  #12 opened 7 years ago by msoos
  0

• digesting output

  #1 opened 8 years ago by NikolajBjorner
  1

• Parser interprets tail of long comment lines as being part of formula

  #4 opened 8 years ago by lammich
  0

• Parser silently overflows on big variable numbers

  #3 opened 8 years ago by lammich
  0

• making it windows / cl friendly

  #2 opened 8 years ago by NikolajBjorner
  0