Release 2.0.0

Release matching the CAV'24 tool paper on CaDiCaL 2.0.

• We have now a contrib directory and for starters there our
  CadiCraig interpolator, which goes through the Tracer API.

• We moved back to use the C99 flexible array member feature in
  Clause which however is not supported by all C++ compiler
  configurations, particularly if compiling in pedantic mode.
  Therefore the configure script checks for support of flexible
  array members and also has a new --no-flexible option.

• Added Dockerfile to support docker containers.

• Added --no-status to skip printing s SATISFIABLE or s UNSATISFIABLE.
  This is useful for online proof checking.

Release 1.9.5

Version 1.9.5

• Removes an unexpected performance regression on the anniversary track
  due to marking forward strengthened redundant clauses as used.

Release 1.9.4

Version 1.9.4

• Simplified code by removing reimply again (but keeping ILB).

Release 1.9.3

Version 1.9.3

• Fixed bogus notification if a user propagator is connected
  with ILB and after local search preprocessing and a second incremental
  call lead to an inconsistent trail to assumption mapping, which might
  have lead to an infinite loop (in very rare cases).

Release 1.9.2

Version 1.9.2

• Important fixes for ILB, trail-reuse and external propagation with
  assumptions.

• Restored effectiveness of Mobical and improved external mock
  propagator.

• Forced garbage collection of binary clauses before restore.

• Merge internal status and state encodings and made them consistent.

• Disabled non-verbose message if empty clause found in input.

• Improved support for IDRUP.

Release 1.9.1

Release 1.9.1

• Fixed position of 'idrup' option.

Release 1.9.0

Version 1.9.0

• Clause IDs in binary LRAT proofs are now always signed.

• Internal CNF regression suite also checks LRAT proofs now.

• Improving the OTFS heuristic (properly bumping literals and
  considering that the conflict clause is updated).

• Making progress to formal 1.9 release with minor fixes for
  different platforms and compilers.

Release 1.8.0

Version 1.8.0

• Explicit Solver::clause functions to simplify clause addition.

• More fine-grained handling of printing proof size information by
  adding bool print = false flags to the flush_proof_trace and
  the close_proof_trace API calls. The former prints the number
  of addition and deletion steps, while the latter prints the size
  of the proof size (and the actual number of bytes if compressed).
  The main effect is that by default printing of proof size disabled
  for API usage but enabled for the stand-alone solver.

Release 1.7.5

Version 1.7.5

• Decreased verbosity level for printing proof size.

Release 1.7.4

Version 1.7.4

• As fork and wait do not exist on Windows writing compressed files
  through pipe/fork/exec/wait has to be disabled for Windows cross
  compilation to go through. Alternatively one could go back to popen
  for writing compressed files on Windows which however is not safe and
  therefore we simply decided to disable that feature for windows.
  Compressed file reading still (and as far we are aware safely) uses
  popen and thus also compiles for Windows.