Home	•	Docs	•	Download	•	Mail	•	FAQ	•	Awards	•	Status	•	MSR

An Efficient SMT Solver

Command line options

Input format

Z3 understands a set of default file extensions, and will invoke a parser based on the extension.

• .dimacs - DIMACS format used by regular SAT solvers.

• .sx, .smp, .simplify - Simplify format.

• .smt - SMT-LIB format.

• .z3 - Z3's native input format.

You can tell Z3 explicitly which grammar the input belongs to by using the following options:

• /d use dimacs parser to read the input file.

• /s use parser for Simplify input format.

• /smt use parser for SMT input format.

• /z3 use parser for Z3 native input format.

Miscellaneous

• /h, ? prints the help message.

• /version prints version number of Z3.

• /v:level be verbose, where <level> is the verbosity level.

• /nw disable warning messages.

• /ini:file configuration file. Several parameters are available besides the ones listed by /h. These parameters can be loaded from an initialization file by using this option.

• /ini? display all available INI file parameters.

The available INI parameters can also be supplied on the command line as a pair parameter-name=parameter-value.

Resources

• /T:timeout set the timeout (in seconds). Setting this option causes the entire process to exit. It is a reliable way to kill Z3.

• /t:timeout set the soft timeout (in seconds). It only kills the current query.

• /memory:bytes set a limit for virtual memory consumption. This limit for virtual memory consumption is approximate, but in general a good guideline for controlling the memory consumption of Z3. If the memory consumption exceeds the specified number of bytes, Z3 exits with a warning message.

Output

• /st display statistics. This option can be used to dump various statistics about the search, such as number of splits, conflict clauses, and quantifier instantiations.

• /m display model. To print a model of a satisfiable (or invalid) formula use this option.

Simplify specific commands

• /cex:num set the maximum number of counter-examples when using Simplify front end. The default number of counter-examples produced when using the Simplify front-end is 1. Use this option to allow returning multiple (independent) counter-examples to invalid formulas.

• /@ only use labels that contain '@' when building multiple counterexamples.

Search heuristics

• /rd:num random case-split frequency (default: 2).

• /rs:num random seed.