NAME

       z3 - a state-of-the art theorem prover from Microsoft Research

SYNOPSIS

       z3 [options] [-file:]file

DESCRIPTION

       This manual page documents briefly the z3 command.

       z3  Z3  is  a  state-of-the  art theorem prover from Microsoft Research. It can be used to
       check the satisfiability of logical formulas over  one  or  more  theories.  Z3  offers  a
       compelling  match  for  software  analysis  and  verification  tools, since several common
       software constructs map directly into supported theories.

Input format

       -smt   Use parser for SMT input format.

       -smt2  Use parser for SMT 2 input format.

       -dl    Use parser for Datalog input format.

       -dimacs
              Use parser for DIMACS input format.

       -log   Use parser for Z3 log input format.

       -in    Read formula from standard input.

Miscellaneous

       -h | -?
              Prints the usage information.

       -version
              Prints version number of Z3.

       -v:level
              Be verbose, where <level> is the verbosity level.

       -nw    Disable warning messages.

       -p     Display Z3 global (and module) parameters.

       -pd    Display Z3 global (and module) parameter descriptions.

       -pm:name
              Display Z3 module <name> parameters.

       -pp:name
              Display Z3 parameter description, if <name> is not provided, then all module  names
              are listed.

       --     All  remaining arguments are assumed to be part of the input file name. This option
              allows Z3 to read files with strange names such as: -foo.smt2.

Resources

       -T:timeout
              Set the timeout (in seconds).

       -t:timeout
              Set the soft timeout (in milli seconds). It only kills the current query.

       -memory:Megabytes
              Set a limit for virtual memory consumption.

Output

       -st    Display statistics.

Parameter setting

       Global and module parameters can be set in the command line.  Use 'z3 -p' for the complete
       list of global and module parameters.

       param_name=value
              For setting global parameters.

       module_name.param_name=value
              For setting module parameters.

AUTHOR

       Z3 Copyright 2006-2014 Microsoft Corp.

       This manual page was written by Michael Tautschnig <mt@debian.org>, for the Debian project
       (and may be used by others).

                                           May 25, 2015                                     Z3(1)