NAME

       cvc3 - automatic SMT theorem prover

SYNOPSIS

       cvc3 [option]... [filename]

DESCRIPTION

       CVC3 is an automated validity checker for a many-sorted (typed) first-order logic with built-in theories,
       including some support for quantifiers, partial functions, and predicate subtypes. The  current  built-in
       theories are the theories of

       •   equality over free (aka uninterpreted) function and predicate symbols,

       •   real and integer linear arithmetic (with some support for non-linear arithmetic),

       •   bit vectors,

       •   arrays,

       •   tuples,

       •   records,

       •   user-defined inductive datatypes.

       CVC3  operates  on files in the CVC Presentation Input Language or the SMTLIB input language. If no input
       file is given on the command line, CVC3 reads standard input.

OPTIONS

       Only a few of the most frequently used options are given below. For more  details,  see  CVC3's  built-in
       help (cvc3 -help) or the CVC3 website.

       -h[elp]
              List all of the options for controlling CVC3. Boolean options are marked (b).  They are enabled by
              prefixing with + and disabled by prefixing with -.  In the help output,  the  current  setting  is
              given.  For example, the output lists

              (b) -interactive      Interactive mode

              Indicating  that interactive mode is disabled. to enable interactive mode, the option +interactive
              is therefore used.  Other options are  marked  (s)  for  string  arguments,  or  (i)  for  integer
              arguments.

       -version
              Print the version of CVC3 and exit.

       -lang  (presentation|smtlib|internal) Select the input language used. The default is presentation.

       +int[eractive]
              Enable interactive mode. Commands are read from standard input and processed immediately.

       +stats Print run-time statistics.

       -timeout t
              Automatically terminate CVC3 after t seconds.

SEE ALSO

       CVC3 website: http://www.cs.nyu.edu/acsys/cvc3/

       SMTLIB website: http://combination.cs.uiowa.edu/smtlib/

AUTHOR

       CVC3  was  written  by  Clark  Barrett,  Cesare  Tinelli, Alexander Fuchs, Yeting Ge, George Hagen, Dejan
       Jovanovic, Sergey Berezin, Cristian Cadar, Jake  Donham,  Vijay  Ganesh,  Deepak  Goyal,  Ying  Hu,  Sean
       McLaughlin, Mehul Trivedi, Michael Veksler, Daniel Wichs, Mark Zavislak, and Jim Zhuang.

       This manual page was written by Dan Sheridan <djs@adelard.com>, for Ubuntu (but may be used by others).

                                                January 16, 2008                                         CVC3(1)