[ANN] Bitwuzla 1.0.0 (SMT solver for AUFBVFP)

On behalf of the bitwuzla team I am pleased to announce the release of bitwuzla ocaml binding (GitHub - bitwuzla/ocaml-bitwuzla: Bitwuzla SMT solver repackaged for convenient use in opam.).

Bitwuzla (https://bitwuzla.github.io/) is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations.

This ocaml binding comes in two flavors:

  • a straight low-level C binding Bitwuzla_c (for the brave and the unaware) – opam depext -i bitwuzla-c;
  • a type-safier OCaml API Bitwuzlaopam depext -i bitwuzla.

(Additionally, you can build bitwuzla standalone executable with opam depext -i bitwuzla-bin.)

Documentation and examples are available online (index (bitwuzla.index)).

Feel free to give it a try,


lol for the name alone.