Release 1.7.3

Version 1.7.3

• Replaced the unsafe popen approach for compressed file writing
  with an explicit pipe/fork/exec/waitpid flow and accordingly
  removed the --safe configuration option again.

Release 1.7.2

Version 1.7.2

• Configuration option --safe disables writing to a file
  through popen which makes library usage safer.

Release 1.7.1

Version 1.7.1

• Added support for VeriPB proofs (--lrat --lratveripb).

• Various fixes: LRAT proofs for constrain (which previously were
  not traced correctly); internal-external mapping issues for LRAT
  (worked for user propagator but now also in combination with LRAT);
  further minor bug fixes.

• Added support for LRAT + external propagator in combination

Release 1.7.0

Merged in the LRAT support by Florian Pollitt (@florianpollitt) as described in our SAT'23 tool paper.

Florian Pollitt, Mathias Fleury and Armin Biere. Faster LRAT Checking than Solving with CaDiCaL.
In Proceedings 26th International Conference on Theory and Applications of Satisfiability Testing,
July 4-8, Alghero, Italy, published by LIPIcs, 2023.

Release 1.6.0

Merged IPASIR-UP theory propagation interface of Katalin Fazekas (@kfazekas) from SAT'23 tool paper:

Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider and Armin Biere.
IPASIR-UP: User Propagators for CDCL. In Proceedings 26th International Conference on Theory and
Applications of Satisfiability Testing, July 4-8, Alghero, Italy, published by LIPIcs, 2023.

Release 1.5.6

Clang-formatted all code (and fixed a spurious regression test failure).

Release 1.5.5

Second intermediate release of our internal branch merge process this summer with on-the-fly self-subsuming resolution and a combination of vivification with instantiation all implemented by @m-fleury

Release 1.5.4

This first intermediate release in the process of merging several branches just merges back the development to the master branch.

Release 1.5.3

First formal release almost identical to 1.5.0 with changes to documentation only but no real algorithmic changes.

Release 1.5.0

This is our FMCAD'21 release which adds a constrain interface to assume single clauses which helps to speed-up SAT based model checking with IC3 and is described in our FMCAD'21 paper.

@inproceedings{FroleyksBiere-FMCAD20,
  author    = {Nils Froleyks and Armin Biere},
  editor    = {Ruzica Piskac and Michael W. Whalen},
  title     = {Single Clause Assumption without Activation Literals to Speed-up {IC3}},
  booktitle = {Proceedings 21st International Conference on Formal Methods in Computer-Aided Design (FMCAD'21)},
  pages     = {72--76},
  volume   = {2},
  publisher = {{TU Vienna Academic Press}},
  year      = {2021}
  doi       = {10.34727/2021/isbn.978-3-85448-046-4_15},
  url       = {https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_15},
}