Artefact to the paper "Lean Certified Bitvector Solving without Bitblasting"

This artefact provides the full results of the evaluation discussed in the paper, scripts used to run it on the bwForCluster Helix (https://wiki.bwhpc.de/e/Helix), and a Dockerfile and corresponding script for running a subset of the evaluated benchmarks on a local machine in reasonable time. Additionally, the implementation of soundness theorems is discussed.

The main part of the artefact, main-artefact.tar.gz, is comprised of the following directories:

cluster: Contains scripts that were used to run the full evaluation on [bwForCluster Helix](https://wiki.bwhpc.de/e/Helix).

local: Contains a Dockerfile for building a Debian-based Docker image with appropriate versions of the used tools (downloaded from the Internet) and scripts for partial local reproduction of the evaluation and plotting of evaluation results.

plots: Contains plots of the full evaluation results, some of which are used in the paper.

summary: Contains generated summaries of the full evaluation results, one input file per line.

Additionally, the full evaluation results are stored in results.tar.gz. They should not be interesting for most users as they are summarised and visualised in the main part of the artefact.

For more information, read the README (available in Markdown, PDF, and HTML) in the main part of the artefact.