Extending DIVINE with Symbolic Verification using SMT (competition contribution)

Authors: Henrich Lauko, Vladimír Štill, Petr Ročkai, Jiří Barnat

DIVINE is an LLVM-based verification tool focusing on analysis of real-world C and C++ programs. Such programs often interact with their environment, for example via inputs from users or network. When these programs are analyzed, it is desirable that the verification tool can deal with inputs symbolically and analyze runs for all inputs. In DIVINE, it is now possible to deal with input data via symbolic computa tion instrumented into the original program at the level of LLVM bitcode. Such an instrumented program maintains symbolic values internally and operates directly on them. Instrumentation allows us to enhance the tool with support for symbolic data without substantial modifications of the tool itself. Namely, this competition contribution uses SMT formulae for representation of input data.

This page corresponds to the submission of DIVINE-SMT to SV-COMP 2019.


DIVINE should work on any reasonably recent Linux distribution. It might also be possible to make it work on macOS, *BSD or even on Windows using Windows Subsystem for Linux, but this is not tested routinely.

Binary Distribution

The binary distribution is intended for SV-COMP and therefore should work on Ubuntu 18.04. However, as a binary distribution, it might not work on other Linux distributions or even on Ubuntu due to updates.

To use it, it is sufficient to extract the archive. Then run ./divine help in the main archive directory. If this succeeds (gives you a list of commands), you should be good to go with the binary distribution, if not, you should build DIVINE from the sources as your system is not compatible with the SV-COMP archive.

Building from Source

To build from the source, you will need some prerequisites, namely a C++11 compiler such as reasonably recent GCC (>= 4.9) or Clang (>= 3.2), make, CMake (>= 3.2), libedit, perl, and about 12GB of disk space and 4GB or RAM. For the symbolic verification to work as in SV-COMP, you will also need the Z3 solver, including its libraries.

You should extract the archive and then run make divine in its main directory. This should build DIVINE into _build.release/tools subdirectory by default. For more details, please refer to the manual.


If you use the binary distribution, both the SV-COMP wrapper (divine-svc) and the main DIVINE binary divine, are located in the divine-svc directory of the archive. If you have built DIVINE from the source, the wrapper resides in tools/divine-svc, while the built binary resides in _build.release/tools/divine.

In order to analyze an SV-COMP benchmark, you will also need a checkout of the SV-Benchmarks repository. Then you can analyze a benchmark as follows:

Where PATH_TO_DIVINE_WRAP is the path where divine-svc resides, PATH_TO_DIVINE_BIN is the path where the binary resides. The last line of the result should be the result given in SV-COMP.

Description of the Wrapper

The divine-svc wrapper handles translation from the SV-COMP property specification to DIVINE’s options and configuration based on some main features of the program.