README

  This is fixed-up version of FuzzSMT based on Robert Brummayer's original 
  fuzzer (for the smt language), and the patch from Christoph Wintersteiger 
  (to handle smt2 language). Below is the original README.   
 
 ******************************************************************************
 *                           FuzzSMT                                          *
 ******************************************************************************

  This is a release of FuzzSMT which is a fuzzing tool for SMT formulas. See
  www.smtlib.org for more details about SMT. For more info about fuzz
  testing SMT solvers see our paper: 'Robert Brummayer and Armin Biere. 
  Fuzzing and Delta-Debugging SMT Solvers', presented at SMT'09. FuzzSMT is
  released under GPL. A copy of the license can be found in the file COPYING. 

  The fuzzer is written in Java 5. I assume that you work on a UNIX/LINUX
  system with Sun's JDK 5 or higher installed.  However, it should be easy
  to follow the introductions and to use FuzzSMT on any other operating
  system that supports Java. Note that if you do not want to compile the
  fuzzer yourself, you just need a compatible Java runtime environment
  (supporting Java 5 or higher) in order to run the fuzzer.

  I use Apache Ant as a build system and I also provide the build-file
  'build.xml'. So, if you want to build the fuzzer, you have to install
  Ant. Then, go to the working directory of FuzzSMT and simply type 'ant'
  to build the fuzzer. For UNIX/LINUX system I provide a simple wrapper
  shell script 'fuzzsmt' which is convenient to use.

  If you want to enable the debugging code of the fuzzer, then enable 
  compilation with debugging info in the build file 'build.xml':

  <javac debug="yes" srcdir="${src}" destdir="${build}"/>

  The code of the fuzzer contains assertions. If you want to enable these
  assertions at run time, you have to call the java interpreter with the
  option '-ea'. Simply add this option to the script 'fuzzsmt'. If you just
  want to run the fuzzer, skip the two steps above.

  In contrast to my previous fuzzing tool called FuzzSMTBV, FuzzSMT is not
  limited to bit-vector theories. Call 'fuzzsmt -h' to get an overview of the
  supported theories. I tried to support all theories that are supported
  by the current version of the SMT-LIB. As you can imagine it was a lot of
  work. I still have some ideas and improvements that I want to implement,
  maybe in future releases.

  The fuzzer has been designed to be highly customizable. Therefore, there
  are many commandline options available. You should experiment with them
  in order to adjust the fuzzer to your needs. Call the fuzzer with '-h' in
  order to get an overview of the available options. As the usage message is
  quite large, it is a good idea to pipe it to a pager such as less. Do not
  worry, each option has a default value, so you do not have to adjust them
  if you do not want to. I tried to configure the fuzzer with reasonable
  default values. So, if you do not want to change the default values,
  just call the fuzzer with the specified logic, e.g. 'fuzzsmt QF_IDL'.

  The fuzzer has been designed to randomize itself. Typically, for each
  option, e.g. the number of variables in the input layer, you can specify
  a minimum and a maximum value. The fuzzer randomly chooses a value within
  this domain.  This takes the load off the user, i.e. the user does not have
  to write a script that randomizes the fuzzer options. If you do not want
  this behavior, e.g. you are interested in random formulas that have exactly
  'n' variables, then simply set the minimum and the maximum value to 'n'.

  If you have comments, questions, improvements or bug reports, then just
  send them to my mail address: robert.brummayer@gmail.com 
  I will try to answer your mails as soon as possible.

  Robert