---
name: "z3"
section: "1"
platform: "linux"
package: "z3"
version: "4.13.3-1"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/z3"
---

# z3(1)

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

## 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).