Compile HiFrog and OpenSMT for Theory Refinement

1. First, install OpenSMT2 as a library to be used in HiFrog binary; configure & install OpenSMT2 as follows:

OpenSMT2 depends on the following libraries:

  • zlib
  • gmp
  • gmpxx
  • readline
  • flex

Guideline to install the requirements:

sudo apt-get update

sudo apt-get install gcc-6

sudo apt-get install g++-6

sudo rm /usr/bin/cpp /usr/bin/gcc /usr/bin/g++

sudo ln -s /usr/bin/cpp-6 /usr/bin/cpp

sudo ln -s /usr/bin/gcc-6 /usr/bin/gcc

sudo ln -s /usr/bin/g++-6 /usr/bin/g++

sudo apt-get install libtool

sudo apt-get install bison flex

sudo apt-get install autoconf

sudo apt-get install git-all


Guideline to Install GMP:


tar Jxvf gmp-6.1.2.tar.xz

cd gmp-6.1.2

./configure --enable-cxx


make check

sudo make install

2. Compile OpenSMT2 for theory refinement as in the following:

$ git clone -b opensmt_SAT2017

Enter the opsntm2 folder and run the configure script:

$ cd opensmt2
$ autoreconf --force --install
$ ./configure

Then run make and install.

$ make
$ sudo make install

3. Download HiFrog:

​  $ git clone -b Theoref_SAT2017

4. Compile Cprover framework in HiFrog repository:

   $ cd hifrog/trunk/cprover/src; make clean; make
4. Compile HiFrog. 
   $ cd funfrog; make clean; make -f Makefile-no-itp

A small hint: During the compilation, if you happen to see such message "make: *** No rule to make target `../cpp/cpp.a', needed by `hifrog'. Stop.", please do "make" in the mentioned directory. Then again do make in funfrog directory.

Run HiFrog to use theory refinement algorithm.

./hifrog --theoref --bitwidth <n> --heuristic <n> --unwind <n> --claim <n> --custom <ids> <your code-to-verify>

./hifrog --theoref --bitwidth 32 --unwind 10 --heuristic 4 --claim 1 filename.c

You may read on the parameters: heuristic, unwind, claim and custom on ./hifrog --help

The git repository we use for HiFrog is hosted at


** If you need any assistance, please contact us **