z3(1)

Usage

z3 [options] [-file:] file

Overview

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.

Releases

Unchanged in 5 releases since Debian 9 (Stretch).

9–13