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


z3 [options] [-file:]file


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

Use parser for SMT input format.
Use parser for SMT 2 input format.
Use parser for Datalog input format.
Use parser for DIMACS input format.
Use parser for Z3 log input format.
Read formula from standard input.


-h | -?
Prints the usage information.
Prints version number of Z3.
Be verbose, where <level> is the verbosity level.
Disable warning messages.
Display Z3 global (and module) parameters.
Display Z3 global (and module) parameter descriptions.
Display Z3 module <name> parameters.
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.


Set the timeout (in seconds).
Set the soft timeout (in milli seconds). It only kills the current query.
Set a limit for virtual memory consumption.


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.
For setting global parameters.
For setting module parameters.


Z3 Copyright 2006-2014 Microsoft Corp.

This manual page was written by Michael Tautschnig <[email protected]>, for the Debian project (and may be used by others).