==============================================================================
README
==============================================================================

CAV 2018 - submission #174

New Word-Level Model Checking Format, Word-Level Model Checker and Bit-Vector Solver

Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere

==============================================================================


0 - Artifact Description
------------------------------------------------------------------------------


OS:
  Arch Linux
  Linux 4.14.15-1-ARCH #1 SMP PREEMPT Tue Jan 23 21:49:25 UTC 2018 x86_64 GNU/Linux

RAM: 32GB
CPU: Ryzen 1800X, 8 Cores, 3.6GHz


VM: default AE virtual machine/unmodified settings

The artifact can be found in the home directory of user 'cav':

  /home/cav/artifact



1 - Getting Started
------------------------------------------------------------------------------

 + Download the VM (cav18ae-174-vm.ova) from directory:

   https://drive.google.com/open?id=1EVene1Cr31oFYr_Th-VuxuQmCdthOZoD


------------------------------------------------------------------------------

2 - Directory Structure of the Artifact
------------------------------------------------------------------------------

The artifact consists of the following four directories:

  + benchmarks/

    Contains all the benchmarks used in the experimental evaluation of our
    paper. We generated these benchmarks from (System) Verilog designs.
    This directory also contains the designs and the scripts to generate the
    BTOR models and SMT2 benchmarks from these designs.
    Please refer to benchmarks/README for details and instructions on how to
    (optionally) generate the benchmarks.


  + paper_experiments/

    Contains a script to re-run and compare the experiments in our paper.
    Please refer to paper_experiments/README for instructions on how to re-run
    and compare the experiments.


  + src/

    Contains source code tree of our SMT solver Boolector. The bounded model
    checker btormc and the witness simulator btorsim are part of the Boolector
    distribution and are built with Boolector.
    The artifact also contains a pre-built Boolector source distribution. If
    you want to re-compile Boolector please refer to src/README for further
    instructions.


  + examples/

    Contains examples for producing witnesses with the bounded model checker
    btormc and checking the witnesses with the witness simulator btorsim.
    Please refer to examples/README for details and instructions on how to
    run the experiments.


  + tools/

    Contains supplementary scripts and binaries required for the artifact and
    are not subject for review.