SYNOPSIS
z3 [options] [-file:]fileDESCRIPTION
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 <[email protected]>, for the Debian project (and may be used by others).