This directory includes the verification files and results of the case studies.
It includes the following sub-directories:

** ic/

  Includes the files from the invertibility conditions case study.

  - generated_smt.tar.xz
    Includes the verification files. These are divided into four directories,
    according to the axiomatization mode (full, partial, combined, qf).

  - cluster_results.tar.xz
    Includes the result files. These are divided into four directories,
    according to the solver and configuration that were used (e.g., vampire,
    cvc4). For every benchmark-solver pair, there are two files: .log and .err,
    corresponding to the output printed to stdout (*.log) and stderr (*.err) of
    the run.


** alive/

  Includes the files from the alive case study.
  The structure of this directory is the same as for directory ic.


** cond_inv/

  This directory contains benchmarks and problems for synthesizing and
  verifying conditional inverses used for the invertibility condition case
  study.

  - cond_inv_synthesis/
    Includes SyGuS input files for synthesizing conditional inverses. It also
    includes the inverses themselves in `sygus_results.csv`, as well as .log
    and .err result files.

  - cond_inv_verification/
    Includes smt2 files for the verification of the conditional inverses. It
    also includes a list of verified inverses in `verified_inverses.csv`, as
    well as .log and .err result files.


** rewrites/

  This directory contains the archive bv_rewrites_results.tar.xz, which
  includes the following two directories:

  - run-ax-initial/
    Benchmarks and results of the first run.

  - run-ax-second/
    Benchmarks with all axioms added from the first run and the corresponding
    results for each solver configuration.

  Each run includes benchmark directories
  rewrites_{formulas2,terms3}_{combined,full,partial,qf} for formula/term
  equivalences with axiomatization modes combined, full, partial and qf.
  Directories run-* contain the log files for each solver configuration run.