package bitwuzla

  1. Overview
  2. Docs
SMT solver for AUFBVFP


Dune Dependency






OCaml binding for the SMT solver Bitwuzla.

Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions and their combinations. Its name is derived from an Austrian dialect expression that can be translated as “someone who tinkers with bits”.



Published: 24 Feb 2023



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.

  (* (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 examples:

  • an incremental example with push and pop (pushpop);

  • an incremental example with check-sat-assuming (checksatassuming);

  • an unsatisfiable example with unsat core generation (unsatcore);

  • an unsatisfiable example with unsat assumption query (unsatassumption).


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

From Opam

opam install 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.3.tbz

:information_source: Handling dependencies with opam

Dependencies can be automatically installed via opam.

opam pin add -n .                             # read the package definition
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 _build/default/_doc/_html/index.html.

Running tests
dune build @runtest

:memo: No output is the expected behavior.

Dependencies (3)

  1. zarith
  2. bitwuzla-c = version
  3. dune >= "2.7"

Dev Dependencies (3)

  1. odoc with-doc
  2. ppx_expect with-test & >= "v0.13"
  3. ppx_inline_test with-test & >= "v0.13"

Used by





Innovation. Community. Security.