Input format
Z3 understands a set of default file extensions, and will invoke a parser based on the extension.
- .smt2 - SMT-LIB 2 format, this is the preferred input format.
- .dimacs, .cnf - DIMACS format used by regular SAT solvers.
- .dl - Datalog input format.
You can tell Z3 explicitly which grammar the input belongs to by using the following options:
- /smt2 use parser for SMT-LIB 2.0 input format.
- /dimacs use dimacs parser to read the input file.
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:Megabytes 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 Megabytes, 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.
Search heuristics
