SMT solver for AUFBVFP (C API)


Bitwuzla is a Satisfiability Modulo Theories
(SMT) solvers for the theories of fixed-size bit-vectors, floating-point
arithmetic, arrays, uninterpreted functions and their combinations.

This library provides an API for using Bitwuzla in OCaml code.
Online documentation is available at


You will want to create some expressions and assert formulas.
For example, consider the following SMT-LIB input:

(set-logic QF_BV)
(set-option :produce-models true)
(declare-const x (_ BitVec 8))
(declare-const y (_ BitVec 8))
        ((_ extract 3 0) (bvsdiv x (_ bv2 8)))
        ((_ extract 3 0) (bvashr y (_ bv1 8)))))

This input is created and asserted as follows:

  (* First, create a Bitwuzla instance. *)
  let open Bitwuzla.Once () in

  (* Create a bit-vector sort of size 8. *)
  let bv8 = 8 in

  (* Create two bit-vector variables of that sort. *)
  let x = Term.const bv8 "x" and y = Term.const bv8 "y" in

  (* Create bit-vector values one and two of the same sort. *)
  let one = bv8 and two = Term.Bv.of_int bv8 2 in

  (* (bvsdiv x (_ bv2 8)) *)
  let sdiv = Term.Bv.sdiv x two in
  (* (bvashr y (_ bv1 8)) *)
  let ashr = Term.Bv.shift_right y one in
  (* ((_ extract 3 0) (bvsdiv x (_ bv2 8))) *)
  let sdive = Term.Bv.extract ~hi:3 ~lo:0 sdiv in
  (* ((_ extract 3 0) (bvashr x (_ sortbv1 8))) *)
  let ashre = Term.Bv.extract ~hi:3 ~lo:0 ashr in

         ((_ extract 3 0) (bvsdiv x (_ sortbv2 8)))
         ((_ extract 3 0) (bvashr y (_ sortbv1 8)))))
  assert' @@ Term.distinct sdive ashre;

After asserting formulas, satisfiability can be determined via

  (* (check-sat) *)
  let result = check_sat () in

If the formula is satifiable, it is possible to query the value
of expressions via get_value as well as its concrete value
via assignment.

  assert (result = Sat);

  (* (get-model) *)
  let xval = get_value x and yval = get_value y in
  Format.printf "assignment of x: %s@\n"
  @@ Z.format "%08b" @@ Term.Bv.assignment xval;
  Format.printf "assignment of y: %s@\n"
  @@ Z.format "%08b" @@ Term.Bv.assignment yval;

It is also possible to query the model value of expressions that do not
occur in the input formula.

  let x2 = Term.Bv.mul x x in
  let x2val = get_value x2 in
  Format.printf "assignment of x * x: %s@\n"
  @@ Z.format "%08b" @@ Term.Bv.assignment x2val;

We can then let the garbage collector delete the Bitwuzla instance,
but if we want to release the resources earlier, it is possible to
call the funcion unsafe_close as the last action of the session.

  (* Finally, delete the Bitwuzla instance. *)
  unsafe_close ()


Other examples together with their SMT-LIB input can be found in directory

  • an incremental example with push and pop

  • an incremental example with check-sat-assuming

  • an unsatisfiable example with unsat core generation

  • an unsatisfiable example with unsat assumption query


Bitwuzla sources and dependencies are repackaged for convenient use
with opam.

From Opam

opam depext -i bitwuzla

From source

The latest version of ocaml-bitwuzla is available on GitHub:

:information_source: Dealing with submodules

In order to checkout the complete source tree,
run the following at clone time:

git clone --recurse-submodules

or at any time:

git submodule init # first time
git submodule update

:warning: Do not download the source archive (.zip, .tar.gz).
Download instead the
tarball from release panel.

tar -xjf bitwuzla-1.0.0.tbz

:information_source: Handling dependencies with opam

Dependencies can be automatically installed via

opam pin add -n .                             # read the package definition
opam depext bitwuzla                          # install system dependencies
opam install --deps-only bitwuzla             # install OCaml dependencies
opam install --deps-only --with-doc bitwuzla  # optional, for documentation
opam install --deps-only --with-test bitwuzla # optional, for tests
dune build @install
Running examples
dune exec -- examples/quickstart.exe # replace quickstart by other examples
Building the API documentation
dune build @doc

An index page containing examples and links to modules can be found in

Running tests
dune build @runtest

:memo: No output is the expected behavior.

with-test & >= "v0.13"
with-test & >= "v0.13"
>= "4.08"
>= "2.7"
Reverse Dependencies
>= "1.0.0" & < "1.0.2"