Reachable State Options:

  -f [<integer bound>]
      Compute forward reachable state first to limit the
      search space.  The optional <integer bound>,
      if specified, will result in bounded model checking;
      i.e., reachable state computation will be limited to
      <integer bound> # of steps from initial states.
      Currently, automatic interpretation of spec checking
      results in bounded model checking is not implemented.
      Thus, you will need to be careful in interpreting
      the result when this <integer bound> option is used.
      When in doubt, don't use the bounded option.
      Overall, when -f is used, the computation generally
      speeds up dramatically.  However, there are cases
      for which the -f flag should not be used.

  -r
      Output the number of states in the reachable space.


Transition Partitioning Options:

  -dp
      Perform disjunctive partitioning.

  -partSize <partition size>
      Limit the graph size of each partition in the transition
      relation.  Use -partSize 0 for monolithic transition
      relation (i.e., no partitioning).  Default value 100000


Variable Ordering Options:

  -i <input variable order file>
      Use <input variable order file> as the initial variable
      ordering.  The variables are listed from the highest to
      the lowest precedence in the ordering.  This list should
      be comma separated and terminated by a semicolon.  All
      white spaces (newline/tab/spaces) are ignored.  All
      comments begin with the '#' character and end with the
      newline character.

  -o <output variable order file>
      Record the result of each variable reordering.  k-th
      variable reordering result is stored in the file
             <output variable order file><k>.ord.
      The file format is the same as described in the -i option.

  -reorder
      This flag enables dynamic variable reordering in
      the BDD package.


Time/Space Limit Options:

  -eTimeOnly
      Replace all calls for CPU time with calls to elapsed time.
      Used to get around SMP Linux's time reporting bug.

  -timeOut <execution time>
      Total CPU execution time bound in seconds.
      Use -timeOut 0 (default) for no time limit.

  -mem <memory limit>
      Set memory usage limit in MBytes.
      Use -mem 0 (default) for no memory limit.


Specifications:

  -spec <num>
      Evaluate only specification number <num>.
      The numbering of specifications starts with 1.
      If <num> is <= 0, then evaluate all specifications.

  -specExistsInit
      Verify the specifications with the SPEC keywords
      as 'there exists an initial state such that the
      specification is true'.  Without this flag, the default
      behavior is 'for all initial states....'.

      Note: the keyword ASPEC can be used (instead of SPEC)
      if a specification is always to be checked under 'for
      all initial states'.  Similarily, ESPEC can be used if a
      specification is always to be checked under 'there
      exists an initial state'.

  -noWitness
      Do not print witness/counter-examples.

  -specOutputLength <length>
      The length of output for specifications.
      For maximum length, set <length> to 0.


Other Optimizations:

  -macro <BDD size limit>
      Enable automatic macro extraction and expansion.
      <BDD size limit> is the BDD graph size limit for any macro.
      <BDD size limit> of 0 disables this optimization.


Debugging Options:

  -v <verbose level>
      Verbose mode showing the progress of the computation
      The higher the <verbose level>, the more information are
      printed.  Use -v 0 (default) to disable the verbose mode
---------------------------------------------------------------------