The tests can be executed by `make test` from a configured build,  the `src`
or `test` directory and will put their intermediate and log files in the
build directory.  If called from outside from the build directory the last
configured build directory is used.

We have four test drivers.  The simplest one

    ./api/run.sh

is going through the API directly to test basic stand-alone functionality of
the library.  Next is a simple usage test for all command line options.

    ./usage/run.sh

The regression suite for CNF files

    ./cnf/run.sh

is more thorough and should catch simple bugs.  It checks solutions and
checks generated proofs too.  The third test driver uses a regression suite
and executes traces by replaying them through `mobical`

    ./traces/run.sh

Last but not least the model based tester `../src/mobical.cpp` is the
most effective test driver and can be run through

    ./mbt/run.sh

All test drivers place their intermediate and logging files into the build
directory.  Thus if for instance you build in a `release` subdirectory
within the root directory of CaDiCaL

    mkdir release
    cd release
    ../configure
    make test

will use the library and binaries in this `release` sub-directory for
running all the tests.  The log files including generated proofs are all put
into the `release` subdirectory too.

For more information on external fuzz-testing see

> Robert Brummayer, Florian Lonsing, Armin Biere:
> Automated Testing and Debugging of SAT and QBF Solvers. SAT 2010: 44-57

Model based testing of SAT solvers is described in

> Cyrille Artho, Armin Biere, Martina Seidl:
> Model-Based Testing for Verification Back-Ends. TAP 2013: 39-55

The simple API test driver and the regression suite are executed by the
default goal of the `makefile`.  There is no need to clean up test output
since it is all put into the build directory.