This is a delta-debugger 'ddsexpr' and a file based fuzzer 'fzsexpr'. In order to configure and compile the programs run ./configure && make Then check out the command line option summaries with ./ddsexpr -h ./fzsexpr -h As a simple example on how to use the program consider that you have an SMT2 benchmark 'bug.smt2' on which the parser of Boolector crashes: # boolector bug.smt2 segmentation fault Then you would call 'ddsexpr' as follows: ddsexpr bug.smt2 red.smt2 boolector This will hopefully reduce the input 'bug.smt2' to a much smaller input file 'red.smt2' on which Boolector produces again the same behavior and most likely due to the same problem; # boolector red.smt2 segmentation fault The reduced file is hopefully much easier to debug. The fuzzer is similar to classical 'real' fuzzer. In particular, it is not a grammer based fuzzer (random input generator) for s-expressions nor SMT files. So typicall you want to invoke it with a set of template files stored in a directory like 'template/'. The fuzzer will mutate those files and givei it to the command specified on the command line. If the exit code makes sense nothing happens, otherwise the mutated file is copied to an output directory and delta-debugged, e.g. fzsexpr template/ output/ boolector is 'our' standard flow of using 'fzsexpr'. This will actually run forever and (hopefully) populate 'output/' with 'bug...' and 'red...' files. In order to limit the number of rounds, use the command line option '-m '. The defaults are to ignore SAT competition exit codes ('0', '1', '10' and '20') and use 'ddsexpr' for delta-debugging. This can however be changed through command line options. See the usage iformation, when running 'fzexpr -h' for more details. See LICENSE for license information. Fri Jan 18 18:59:39 CET 2013 Armin Biere, FMV, JKU