Building Yices from Source
git clone https://github.com/SRI-CSL/yices2.git
You can choose between different compile-time features and optional components:
Support for the MCSAT solver (necessary for non-linear arithmetic).
Support for back-end Boolean SAT solvers (which can provide performance improvements on bit-vector problems).
Build a thread-safe version of the Yices library.
The following build instructions are written for Ubuntu but they should work with minor adjustments on other Unix variants. For Windows, we recommand compiling using Cygwin or with the MinGW cross-compilers.
No matter which variant you want to build, you need a C compiler that
supports C99. Any reasonably recent version of GCC or Clang should
work. You will also need standard build tools such as
GNU Make and
If you cloned the GitHub repository, you will also need autoconf.
The simplest type of build does not include MCSAT or third-party SAT solvers. Start by installing the dependencies:
sudo apt-get install libgmp-dev sudo apt-get install gperf
Build from a source tarfile
If you donwloaded the source tarfile from https://yices.csl.sri.com, you can configure and build Yices as follows:
./configure make -j sudo make install
This installs the binaries in
/usr/local/bin, the header files
/usr/local/include, and the library in
/usr/local/lib. You can change the installation location by
giving the option
--prefix=<directory> to the
Build from a clone of our Git repository
If you got the source from our GitHub repository, the build process is almost
the same as from a tarfile. Make sure
autoconf is installed:
sudo apt-get install autoconf
Then build Yices as follows:
autoconf ./configure make -j sudo make install
Running the tests
Optionally, you can check that the build was fine by using
This will run the Yices regression tests.
The MCSAT solver has two more dependencies:
The LibPoly library for manipulating polynomials.
The CUDD libray for Binary Decision Diagrams.
Get LibPoly from our GitHub repository and follow the build instructions there. Make sure to get the latest LibPoly release.
We recommend clone the CUDD Git repository from https://github.com/ivmai/cudd
CUDD must be built as Position-Independent Code (i.e., with option
-fPIC) to be linked
Here is how you can build CUDD:
git clone https://github.com/ivmai/cudd cd cudd ./configure CFLAGS=-fPIC make sudo make install
This will install CUDD header files and libraries in /usr/local.
The CUDD Makefile was created with
automake-1.14. Compilation may
fail if you have a different version of
automake with a complaint
WARNING ’automake-1.14’ is missing on your system. If this
happens to you, try this before you type
Configure and Build Yices with MCSAT Support
Once you’ve installed LibPoly and CUDD, you can build Yices as follows:
./configure --enable-mcsat make -j sudo make install
You may need to set CPPFLAGS and LDFLAGS if the libpoly library is not in a standard location.
Third-Party SAT Solvers
Yices can use third-party SAT solvers as backends to the bit-vector solvers. We call these delegates. Currently two third-party solvers are supported
You can compile Yices with one or both of these SAT solvers.
CaDiCaL must be built with option
-fPIC to work with Yices. It’s
also a good idea to install CaDiCaL in a standard location such as
/usr/local. If you use
bash, the following instructions
git clone https://github.com/arminbiere/cadical cd cadical CXXFLAGS=-fPIC ./configure make make test sudo install build/libcadical.a /usr/local/lib sudo install build/cadical build/mobical /usr/local/bin sudo install -m644 src/ccadical.h /usr/local/include
Yices requires a patched version of CryptoMiniSAT 5 that we provide at https://github.com/BrunoDutertre/cryptominisat. You may also need to install CryptoMiniSAT’s dependencies:
sudo apt-get install cmake zlib1g-dev libboost-program-options-dev
Then you can build and install CryptoMiniSAT as follows:
git clone https://github.com/BrunoDutertre/cryptominisat cd cryptominisat mkdir build cd build cmake .. -DENABLE_PYTHON_INTERFACE=OFF make sudo make install
This will install CryptoMiniSAT in
There are more detailed build instructions in the CryptoMiniSAT
Configure and Build Yices with Third-Party Solvers
To build Yices with support for both CaDiCaL and CryptoMiniSAT, use the following configure command in the top-level yices source directory:
./configure CPPFLAGS='-DHAVE_CADICAL -DHAVE_CRYPTOMINISAT' \ LIBS=’-lcryptominisat5 -lcadical -lstdc++ -lm’
If you want only CaDiCaL:
./configure CPPFLAGS=-DHAVE_CADICAL LIBS=’-lcadical -lstdc++ -lm’
If you want only CryptoMiniSAT:
./configure CPPFLAGS=-DHAVE_CRYPTOMINISAT LIBS=’-lcryptominisat5 -lstdc++’
After any of these
configure commands, you can build Yices as usual:
make -j sudo make install
These third-party solvers are compatible with MCSAT. So you can add
--enable-mcsat to also include support for MCSAT.
Thread-Safe Yices Library
By default, the Yices library is not re-entrant and should not be used in multithreaded applications. If you need a thread-safe version of the library, configure and build Yices as follows:
./configure --enable-thread-safety make -j sudo make install
When configured in this way, the Yices library allows multiple threads
to operate on separate contexts and models without causing race
conditions. This is useful to call
different contexts in parallel. API functions that create terms and
types are automatically serialized by an internal locking mechanism.
It is not safe for distinct threads to operate on the same context or model concurrently. It you want to do that, you have to implement your own locking mechanism.
--enable-mcsat options are
currently incompatible. It is not possible to build a Yices version
that is both thread-safe and support MCSAT.