Build Guide

ESBMC builds on Linux, macOS, FreeBSD and Windows. Pick your platform below and follow the steps. Each tab produces a working esbmc with the Z3 solver; the heavier dependencies (LLVM/Clang, fmt, nlohmann-json, yaml-cpp and immer) are downloaded and built automatically with -DDOWNLOAD_DEPENDENCIES=1 where the platform supports it.

At least 6 GB of RAM is recommended. ESBMC is distributed mainly under

the Apache License 2.0.

For a build with several solvers, or CHERI/fuzzing support, see Building with all solvers and Advanced.

Build ESBMC

Install prerequisites

sudo apt-get update
sudo apt-get install -y build-essential cmake ninja-build git bison flex python3 libboost-all-dev g++-multilib

LLVM/Clang, Z3 and the libraries fmt, nlohmann-json, yaml-cpp and immer are fetched by -DDOWNLOAD_DEPENDENCIES=1, so they are not installed here.

Get the source

git clone https://github.com/esbmc/esbmc.git
cd esbmc

Configure and build

cmake -GNinja -Bbuild -DDOWNLOAD_DEPENDENCIES=1 -DENABLE_Z3=1
ninja -C build

The binary is written to build/src/esbmc/esbmc.

Optional: run the regression tests

Add the testing flags when configuring, then run ctest:

CXX=g++ CC=gcc cmake -GNinja -Bbuild -DDOWNLOAD_DEPENDENCIES=1 -DENABLE_Z3=1 -DBUILD_TESTING=On -DENABLE_REGRESSION=On
ninja -C build
ctest --test-dir build -j"$(nproc)" -L esbmc --timeout 120

Optional: enable a frontend or extra solvers

For Python, Solidity or IBEX support see Optional frontends. For a multi-solver build see Building with all solvers.

Install prerequisites

sudo dnf install gcc-c++ cmake ninja-build git bison flex python3 boost-devel z3-devel glibc-devel.i686 libstdc++-devel.i686

LLVM/Clang, fmt, nlohmann-json, yaml-cpp and immer are fetched by -DDOWNLOAD_DEPENDENCIES=1; Z3 comes from the system z3-devel package. The flag is required on Fedora because immer has no Fedora package. glibc-devel.i686 and libstdc++-devel.i686 are the 32-bit C runtime headers used to build ESBMC’s 32-bit operational models.

Get the source

git clone https://github.com/esbmc/esbmc.git
cd esbmc

Configure and build

CXX=g++ CC=gcc cmake -GNinja -Bbuild -DDOWNLOAD_DEPENDENCIES=1 -DENABLE_Z3=1 -DBUILD_TESTING=On -DENABLE_REGRESSION=On
ninja -C build

The binary is written to build/src/esbmc/esbmc.

Optional: skip 32-bit support

If you do not need 32-bit verification, drop the two .i686 packages and add -DENABLE_BUNDLE_LIBC_32BIT=Off.

Optional: enable a frontend or extra solvers

For Python, Solidity or IBEX support see Optional frontends. For a multi-solver build see Building with all solvers.

Install prerequisites

brew install llvm@21 z3 boost cmake ninja python bison

On macOS, -DDOWNLOAD_DEPENDENCIES must be combined with -DLLVM_DIR

so only the portable libraries are downloaded — the prebuilt LLVM/Z3 it would otherwise fetch are Linux binaries.

Get the source

git clone https://github.com/esbmc/esbmc.git
cd esbmc

Configure and build

cmake -GNinja -Bbuild -DDOWNLOAD_DEPENDENCIES=1 -DENABLE_Z3=1 \
  -DLLVM_DIR=$(brew --prefix llvm@21)/lib/cmake/llvm \
  -DClang_DIR=$(brew --prefix llvm@21)/lib/cmake/clang \
  -DZ3_DIR=$(brew --prefix z3)
ninja -C build

Easiest: use the helper script

The repository ships scripts/build-esbmc-mac.sh, which creates the build folder, optionally installs Boolector/Bitwuzla, and installs esbmc globally:

./scripts/build-esbmc-mac.sh

Xcode SDK

A full Xcode or the Command Line Tools SDK is required — macOS keeps the C library headers inside the SDK rather than in /usr/include. CMake detects it automatically (CMAKE_OSX_SYSROOT, then xcrun --show-sdk-path) and stores it in C2GOTO_SYSROOT; pass -DC2GOTO_SYSROOT=<path to MacOSX.sdk> only to override that choice. If xcrun --show-sdk-path fails, install the tools with xcode-select --install.

A build that ends up with no SDK fails while generating the libc models, with complex.c:1:10: fatal error: 'complex.h' file not found.

Install prerequisites

pkg install git cmake ninja python3 z3 bison flex boost-all

ESBMC needs 32-bit libraries on FreeBSD — make sure the lib32 set is installed.

Provide an LLVM/Clang toolchain

ESBMC’s prebuilt LLVM download targets Linux, so fetch a FreeBSD LLVM release and point the build at it:

fetch https://github.com/llvm/llvm-project/releases/download/llvmorg-16.0.0/clang+llvm-16.0.0-amd64-unknown-freebsd13.tar.xz
tar xf clang+llvm-16.0.0-amd64-unknown-freebsd13.tar.xz
mv clang+llvm-16.0.0-amd64-unknown-freebsd13 clang16

Get the source, configure and build

git clone https://github.com/esbmc/esbmc.git && cd esbmc
cmake -GNinja -Bbuild -DDOWNLOAD_DEPENDENCIES=1 -DENABLE_Z3=1 -DZ3_DIR=/usr/local \
  -DLLVM_DIR=$PWD/../clang16 -DClang_DIR=$PWD/../clang16
ninja -C build

Install the toolchain

Visual Studio with the Desktop development with C++ workload (install the English language pack even on non-English systems).
Chocolatey and vcpkg (integrate vcpkg with your system).
Check the repository out with LF line endings — CRLF will not work.

Install dependencies

vcpkg.exe install boost-filesystem:x64-windows boost-date-time:x64-windows boost-test:x64-windows boost-multi-index:x64-windows boost-crc:x64-windows boost-property-tree:x64-windows boost-uuid:x64-windows
choco install winflexbison gnuwin32-coreutils.portable

Also obtain Z3 and a prebuilt LLVM/Clang. The official LLVM releases do not ship the CMake modules ESBMC needs, so build LLVM from source (see below).

Configure and build

Open the CMake project in Visual Studio, set the configuration to Release, the toolchain to msvc_x64_x64, the triplet to x64-windows, and add the dependency paths to the CMake flags:

-DLLVM_DIR=C:\Deps\llvm -DClang_DIR=C:\Deps\llvm -DZ3_DIR=C:\Deps\z3

Build LLVM/Clang from source on Windows

Download the llvm-14.X.X.src and clang-14.X.X.src archives from the LLVM releases and unpack each into its own space-free directory. Then, from the x64 Native Tools Command Prompt for VS 2019:

mkdir llvm-14.0.6.src\build-release && cd llvm-14.0.6.src\build-release
cmake .. -Thost=x64 -G "Visual Studio 16 2019" -A x64 ^
  -DCMAKE_INSTALL_PREFIX=C:\Deps\llvm -DCMAKE_PREFIX_PATH=C:\Deps\llvm ^
  -DLLVM_ENABLE_ZLIB=OFF -DLLVM_ENABLE_LIBXML2=OFF ^
  -DCMAKE_BUILD_TYPE=Release -DLLVM_USE_CRT_RELEASE=MT
msbuild /m -p:Configuration=Release INSTALL.vcxproj

Repeat for the clang-14.X.X.src tree (same flags) to install Clang into the same prefix.

Build inside WSL

With WSL you can build ESBMC exactly as on Linux — follow the Ubuntu / Debian tab.

Debugging the C++ frontend

A debug build of Clang greatly helps when debugging ESBMC’s Clang-based C++ converter, since it lets you step into the Clang AST as ESBMC walks it. See Rafael’s guide for building LLVM from source.

Dependency reference

package	required	minimum version
clang	yes	18.0.0
boost	yes	1.77
CMake	yes	3.18.0
Boolector	no	3.2.2
CVC4	no	1.8
CVC5	no	1.1.2
MathSAT	no	5.5.4
Yices	no	2.6.4
Z3	no	4.13.3
Bitwuzla	no	0.9.0

The version requirements are stable but can change between releases. For all available CMake options, see Options.cmake.

Optional frontends

These are extra CMake flags added to the configure step in any platform tab above.

Python

Add -DENABLE_PYTHON_FRONTEND=On to the configure step:

cmake -GNinja -Bbuild -DDOWNLOAD_DEPENDENCIES=1 -DENABLE_Z3=1 -DENABLE_PYTHON_FRONTEND=On

ast2json is vendored in the source tree, so no pip install is needed. Optionally install mypy (e.g. pipx install mypy) for Python type checks.

Solidity

Add -DENABLE_SOLIDITY_FRONTEND=On to the configure step. The Solidity frontend verifies smart contracts against predefined safety properties (bounds, overflow, underflow) and user-defined assertions.

IBEX (interval constraint solving)

Enables --goto-contractor. Install IBEX following its instructions, then:

cmake -GNinja -Bbuild -DENABLE_GOTO_CONTRACTOR=ON -DIBEX_DIR=path-to-ibex

API documentation

Add -DBUILD_DOC=On to the configure step to build the Doxygen API reference alongside ESBMC (requires doxygen and graphviz). See the API Reference guide for details.

Building with all solvers

ESBMC supports Bitwuzla, Boolector, CVC4, CVC5, MathSAT, Yices 2 and Z3. All are optional, but without at least one solver ESBMC cannot verify most programs. For a single-solver build, the platform tabs above are enough.

ESBMC can additionally drive Bitwuzllob — Bitwuzla running on the massively parallel Mallob platform — as an external process; see Using Bitwuzllob below. It needs no build-time setup (the backend is enabled by default, -DENABLE_BITWUZLLOB=ON).

The recipe below mirrors the multi-solver build used in ESBMC’s CI: build each solver into the project directory, then point the configure step at them. Build only the solvers you need.

Prepare a Clang/LLVM toolchain

For a static build, let ESBMC download Clang/LLVM:

ESBMC_CLANG=-DDOWNLOAD_DEPENDENCIES=On
ESBMC_STATIC=ON

A static build passes -static to the linker, so every system library ESBMC (and the downloaded LLVM) depends on must be available as a static archive. On Ubuntu, make sure the .a variants are installed, e.g. sudo apt-get install zlib1g-dev (provides libz.a); without it the configure step fails with ld: attempted static link of dynamic object .../libz.so. If in doubt, use the shared build below, or drive the static build through ./scripts/build.sh, which provisions the static toolchain the same way ESBMC’s release CI does.

For a shared build, use the system LLVM/Clang instead. Because this recipe does not pass -DDOWNLOAD_DEPENDENCIES, the fmt, nlohmann-json, yaml-cpp and immer libraries must also come from the system. Use Clang 18 or newer: current ESBMC uses the C++23 explicit-object-parameter (“deducing this”) API added in Clang 18, so older toolchains such as llvm-16 no longer compile it and fail with 'clang::CXXMethodDecl' has no member named 'isExplicitObjectMemberFunction'. ESBMC’s CI builds this configuration with Clang 21; any version >= 18 works. Ubuntu example:

sudo apt-get install libclang-18-dev libclang-cpp18-dev \
  libfmt-dev nlohmann-json3-dev libyaml-cpp-dev libimmer-dev
ESBMC_CLANG="-DLLVM_DIR=/usr/lib/llvm-18/lib/cmake/llvm -DClang_DIR=/usr/lib/cmake/clang-18"
ESBMC_STATIC=OFF

libclang-18-dev ships /usr/lib/cmake/clang-18/ClangConfig.cmake, which find_package(Clang) needs; without it the configure step fails with Could not find a package configuration file provided by "Clang". Depending on how your system LLVM was packaged you may also need libzstd-dev and libcurlpp-dev, which its CMake targets pull in. If your distribution does not package Clang 18 or newer, install one from https://apt.llvm.org and bump the version number in the package names and paths above.

Keep LLVM_DIR and Clang_DIR on the same toolchain version. Mixing them (e.g. LLVM_DIR on llvm-16 while Clang_DIR is clang-18) links libLLVM-16 against libclang-cpp-18 and fails late with undefined reference … DSO missing from command line; ESBMC now stops such a configuration at CMake time. When switching compiler versions, reconfigure in a fresh build directory — a stale CMakeCache.txt keeps the old paths.

Build the solvers

Boolector

git clone --depth=1 --branch=3.2.3 https://github.com/boolector/boolector && cd boolector && ./contrib/setup-lingeling.sh && ./contrib/setup-btor2tools.sh && ./configure.sh --prefix $PWD/../boolector-release && cd build && make -j9 && make install && cd ../..

# Linux
wget https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-glibc-2.35.zip && unzip z3-4.13.3-x64-glibc-2.35.zip && mv z3-4.13.3-x64-glibc-2.35 z3
# macOS
brew install z3 && cp -rp $(brew info z3 | egrep "/usr[/a-zA-Z\.0-9]+ " -o) z3

Bitwuzla

Requires MPFR >= 4.2.1 (apt-get install libmpfr-dev / brew install mpfr) and Meson (pip install meson).

git clone --depth=1 --branch=0.9.0 https://github.com/bitwuzla/bitwuzla.git && cd bitwuzla && ./configure.py --prefix $PWD/../bitwuzla-release && cd build && meson install && cd ../..

CVC4 (Linux only)

pip3 install toml && git clone https://github.com/CVC4/CVC4.git && cd CVC4 && git reset --hard b826fc8ae95fc && ./contrib/get-antlr-3.4 && ./configure.sh --optimized --prefix=../cvc4 --static --no-static-binary && cd build && make -j4 && make install && cd ../..

CVC5

pip3 install toml && git clone https://github.com/CVC5/CVC5.git && cd CVC5 && git switch --detach cvc5-1.1.2 && ./configure.sh --prefix=../cvc5 --auto-download --static --no-static-binary && cd build && make -j4 && make install && cd ../..

MathSAT

# Linux
wget http://mathsat.fbk.eu/release/mathsat-5.5.4-linux-x86_64.tar.gz -O mathsat.tar.gz && tar xf mathsat.tar.gz && mv mathsat-5.5.4-linux-x86_64 mathsat
# macOS
wget http://mathsat.fbk.eu/release/mathsat-5.5.4-darwin-libcxx-x86_64.tar.gz -O mathsat.tar.gz && tar xf mathsat.tar.gz && mv mathsat-5.5.4-darwin-libcxx-x86_64 mathsat && ln -s /usr/local/include/gmp.h mathsat/include/gmp.h

Yices (Linux)

Yices needs a static GMP first:

wget https://gmplib.org/download/gmp/gmp-6.1.2.tar.xz && tar xf gmp-6.1.2.tar.xz && cd gmp-6.1.2 && ./configure --prefix $PWD/../gmp --disable-shared ABI=64 CFLAGS=-fPIC CPPFLAGS=-DPIC && make -j4 && make install && cd ..
git clone https://github.com/SRI-CSL/yices2.git && cd yices2 && git checkout Yices-2.6.4 && autoreconf -fi && ./configure --prefix $PWD/../yices --with-static-gmp=$PWD/../gmp/lib/libgmp.a && make -j9 && make static-lib && make install && cp ./build/x86_64-pc-linux-gnu-release/static_lib/libyices.a ../yices/lib && cd ..

Configure and build ESBMC

Pass the directories of the solvers you built. Drop the flags for any solver you skipped.

cd esbmc && cmake -GNinja -Bbuild -DBUILD_TESTING=On -DENABLE_REGRESSION=On \
  $ESBMC_CLANG -DBUILD_STATIC=${ESBMC_STATIC:-ON} \
  -DBoolector_DIR=$PWD/../boolector-release -DZ3_DIR=$PWD/../z3 \
  -DENABLE_MATHSAT=ON -DMathsat_DIR=$PWD/../mathsat \
  -DENABLE_YICES=On -DYices_DIR=$PWD/../yices -DCVC4_DIR=$PWD/../cvc4 \
  -DGMP_DIR=$PWD/../gmp -DBitwuzla_DIR=$PWD/../bitwuzla-release \
  -DCMAKE_INSTALL_PREFIX:PATH=$PWD/../release
ninja -C build && ninja -C build install

ESBMC is installed into the release folder. Add -DCMAKE_BUILD_TYPE=Debug to enable ESBMC’s internal assertions.

Using Bitwuzllob

Bitwuzllob (Schreiber, Niemetz, Preiner — TACAS'26) integrates Bitwuzla into the massively parallel Mallob platform, distributing the bit-blasted SAT queries across hundreds of cores. Mallob is an MPI program that cannot be linked into ESBMC, so the --bitwuzllob backend writes the verification condition to an SMT-LIB2 file and runs Mallob’s one-shot mono mode on it as an external process. Notes:

Linux only (Mallob supports x86/ARM Linux). Build Mallob with the SMT application engine following the artifact of the TACAS'26 paper (https://doi.org/10.5281/zenodo.17478480), and make sure the mallob binary and its MPI runtime are available.
The command is configurable via --bitwuzllob-prog; every %f is replaced by the formula file (default: mallob -mono=%f -mono-app=SMT). For example: esbmc file.c --bitwuzllob --bitwuzllob-prog "mpirun -np 8 mallob -mono=%f -mono-app=SMT".
A terminated mono process cannot answer model queries, so building a counterexample additionally needs a local interactive SMT-LIB2 solver via --bitwuzllob-model-prog (e.g. "z3 -in" or "bitwuzla"); it replays the same formula and serves the (get-value ...) queries. Alternatively pass --result-only to skip the counterexample.
One-shot mono mode serves a single (check-sat), so incremental strategies (--incremental-bmc, --k-induction, …) are rejected — use a linked solver such as --bitwuzla for those. Like Bitwuzla, Bitwuzllob is bit-vector-only and cannot serve --ir/--ir-ieee.

Advanced

Build in a Docker container

A minimal Debian-based image that builds ESBMC with Z3, letting -DDOWNLOAD_DEPENDENCIES=1 fetch LLVM/Clang and the libraries:

FROM ubuntu:24.04
RUN apt-get update && apt-get install -y --no-install-recommends \
      build-essential cmake ninja-build git bison flex \
      python3 libboost-all-dev g++-multilib \
    && rm -rf /var/lib/apt/lists/*
RUN git clone --depth=1 https://github.com/esbmc/esbmc.git /esbmc
WORKDIR /esbmc
RUN cmake -GNinja -Bbuild -DDOWNLOAD_DEPENDENCIES=1 -DENABLE_Z3=1 \
    && ninja -C build

Build the image with docker build -t esbmc .; the binary is at /esbmc/build/src/esbmc/esbmc.

Shared (dynamic) builds

A non-static ESBMC links against system libraries/solvers. Shared linking is the default when CMake is invoked with -DBUILD_STATIC=Off (or the variable unset).

When Clang is built with CLANG_LINK_CLANG_DYLIB=On, ESBMC links the dynamic libclang-cpp and does not bundle Clang’s headers. Header bundling is controlled by CLANG_HEADERS_BUNDLED (On/Off/detect); the default detect bundles headers only for static Clang links. Not bundling speeds up source translation by avoiding a temporary header-extraction directory, but ESBMC must be recompiled when the system Clang is updated.

CHERI-C support (experimental)

CHERI-enabled ESBMC uses CHERI Clang (release 20210817, clang 13). Build it, then configure ESBMC against it:

wget https://github.com/CTSRD-CHERI/llvm-project/archive/refs/tags/cheri-rel-20210817.tar.gz
sudo apt-get install lld
tar xf cheri-rel-20210817.tar.gz && mkdir clang13 && cd llvm-project-cheri-rel-20210817 && mkdir build && cd build
cmake -GNinja -S ../llvm -DCMAKE_BUILD_TYPE=Release -DLLVM_ENABLE_PROJECTS='llvm;clang' -DLLVM_INSTALL_BINUTILS_SYMLINKS=TRUE -DLLVM_ENABLE_LIBXML2=FALSE -DLLVM_ENABLE_ZLIB=FALSE '-DLLVM_TARGETS_TO_BUILD=AArch64;ARM;Mips;RISCV;X86;host' -DCMAKE_INSTALL_PREFIX=../../clang13
ninja && ninja install && cd ../..
ESBMC_CLANG=$(echo -D{LLVM,Clang}_DIR=$PWD/clang13)

A CHERI sysroot is needed for programs that use the C standard library. The cheribuild tool is the recommended way to obtain one:

git clone https://github.com/CTSRD-CHERI/cheribuild.git && cd cheribuild && python3 cheribuild.py cheribsd-sdk-riscv64-purecap -d

Then configure ESBMC with:

-DESBMC_CHERI=On -DESBMC_CHERI_HYBRID_SYSROOT=<path> -DESBMC_CHERI_PURECAP_SYSROOT=<path>

e.g. <path> pointing at $HOME/cheri/output/sdk/sysroot-riscv64-purecap.

Fuzzing targets

ESBMC ships libFuzzer targets. They must be built with Clang, so configure ESBMC to use it and enable fuzzing:

cmake -GNinja -Bbuild -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DENABLE_FUZZER=1

Passing the compiler options for the first time clears the CMake cache, so some variables may need to be re-set.

Architecture