******************************************************************************
 *                           FuzzSMTBV                                        *
 ******************************************************************************

  This is a release of FuzzSMTBV which is a fuzzing tool for SMT formulas
  that contain bit-vectors and bit-vector arrays. 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. FuzzSMTBV is released under GPL. A copy
  of the license can be found in the file COPYING.

  FuzzSMTBV is my first fuzzer prototype. It is a lightweight fuzzer and is
  limited to the bit-vector theories QF_BV and QF_AUFBV. My second fuzzing
  tool FuzzSMT is more generic and sophisticated. It supports a large number
  of theories, including the two mentioned above. I recommend using my 
  second fuzzing SMT tool which is available at http://fmv.jku.at/fuzzsmt
  Nevertheless, FuzzSMTBV is a nice fuzzer prototype which can be all you
  need if you are looking for a light-weight SMT fuzzer for bit-vectors and 
  arrays. Of course you can use both FuzzSMT and FuzzSMTBV, which is exactly
  what I do in order to test my SMT solver Boolector. FuzzSMTBV is written
  in Python 2 and has been tested with Python 2.5.2.

  The fuzzer has been designed to be customizable. Therefore, there are many
  command line options available. You should experiment with them in order
  to adjust the fuzzer to your needs.  Call the fuzzer with '-h' to get an
  overview of the available options. Each option has a default value, so you
  do not have to adjust all of them. 

  Unlike FuzzSMT, FuzzSMTBV has not been designed to randomize its options.
  For example, the default number of variables is set to 5, i.e. the fuzzer
  will generate random instances with exactly 5 variables in the input
  layer. In order to increase randomness, I recommend varying the command
  line options of the fuzzer. In order to vary the number of variables,
  write a simple shell script that generates a random number 'n' which is
  for instance between 1 and 5. Then, from your script, call the fuzzer
  with the argument '-v' in order to tell the fuzzer that it should use 'n'
  variables. In this way, you get formulas that contain 1 to 5 variables
  and you may find further defects that you have not found before.

  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