SVComp

Run SVComp Benchmarks

Ultimate allows the user to run benchmarks provided by the Software Verification Competition (SVComp). This page will explain how to check out the benchmarks from their official repository (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks) and how to use Ultimate to verify the benchmarks.

Checking out the Repository and Creating the Necessary Links

In the official SVComp benchmark repository, there are different sets of benchmarks that can be used for different purposes. This guide only focuses on the benchmarks written in C.

1. Create a directory for the benchmarks

   cd /some/toplevel/directory
   mkdir svcomp

2. Create a fresh git repository

   cd svcomp
   git init

3. Add the remote from where to pull later

   git remote add origin https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks.git

4. In order to conserve space on the hard disk, only the c/ directory is going to be checked out. Therefore, it is necessary to tell git to perform a sparse checkout later

   git config --local core.sparsecheckout true
   echo c/ >> .git/info/sparse-checkout

5. Pull the repository without the history

   git pull origin main --depth=1

After that, the repository should be pulled, while only the c/ directory is being checked out. The space that is being used up should be somewhere around 5 GB.

In order for Ultimate's test suites to run correctly, the svcomp benchmarks need to be located in /trunk/examples/svcomp. You can accomplish this by adding a symlink:

ln -s /some/toplevel/directory/svcomp/c /path/to/ultimate/repository/trunk/examples/svcomp

Useful git commands

Change of the sparse-checkout File

In case you need to change the sparse-checkout file for some reason, you need to issue the following command after the change in order for git to still work with the sparse checkout:

cd /some/toplevel/directory/svcomp
git read-tree -mu HEAD

Windows

If you are using windows, this guide is the same for all the git-related commands. The commands themselves can be issued from a command prompt (cmd.exe).

To create the link of the SVComp directory to the examples directory of Ultimate, use the following command from an Administrator command prompt (Click Start, enter "cmd" right click on the appearing command, select "Run as Administrator"):

mklink /D Drive:\path\to\ultimate\repository\trunk\examples\svcomp Drive:\some\toplevel\directory\svcomp\c