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 generated proofs too. The third test driver uses a regression suite uses regression execution traces by replaying them through `mobical` ./traces/run.sh Last but not least the model based tester `../src/mobical.cpp` however is 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 and 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.