z3 - Man Page

manual page for Z3 version 4.12.1 — 64 bit


z3 [options] [-file:]file


Z3 [version 4.12.1 - 64 bit]. (C) Copyright 2006-2016 Microsoft Corp.

Input format


use parser for SMT 2 input format.


use parser for Datalog input format.


use parser for DIMACS input format.


use parser for Weighted CNF DIMACS input format.


use parser for PB optimization input format.


use parser for a modest subset of CPLEX LP input format.


use parser for Z3 log input format.


read formula from standard input.


display model for satisfiable SMT.


-h,  -?

prints this message.


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 module ('name') parameters in Markdown format.


display Z3 parameter description, if 'name' is not provided, then all module names are listed.


display built-in tactics or if argument is given, display detailed information on tactic.


display avilable probes.


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.


for setting global parameters.


for setting module parameters.

Use 'z3 -p' for the complete list of global and module parameters.


January 2023 Z3 version 4.12.1 - 64 bit