Compile HiFrog for Theory Refinement


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

​​OpenSMT2 depends on the libraries: zlibgmp,gmpxxreadlineflex. If you do not have them installed, please first check installation guide here, then continue the following steps:

To compile OpenSMT2, first download it via:

$ git clone

Enter the opsntm2 folder and run the configure script:

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

Then run make and install.

$ make
$ sudo make install

2. Get the git repository of hifrog:

​  $ git clone -b master

3. Compile the cprover framework in the hifrog repository:

   $ cd hifrog/trunk/cprover/src; make clean; make
4. Check the in hifrog/trunk/cprover/src/Makefile and 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 **

sepideh.a65[at] or karine.even_mendoza[at]