Man Linux: Main Page and Category List


       cvc3 - automatic SMT theorem prover


       cvc3 [option]... [filename]


       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

       ·   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.


       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

              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.

              Print the version of CVC3 and exit.

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

              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.


       CVC3 website:

       SMTLIB website:


       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  <>,  for
       Ubuntu (but may be used by others).

                               January 16, 2008