# z3 / src / shell / options.h

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67  /** \page cmdline Command line options \section informat Input format Z3 understands a set of default file extensions, and will invoke a parser based on the extension. - \ext{smt2} - SMT-LIB 2 format, this is the preferred input format. - \ext{dimacs}, \ext{cnf} - DIMACS format used by regular SAT solvers. - \ext{dl} - Datalog input format. - \ext{smt} - (deprecated) SMT-LIB 1 format. You can tell Z3 explicitly which grammar the input belongs to by using the following options: \cmdopt{smt2} use parser for SMT-LIB 2.0 input format. \cmdopt{dimacs} use dimacs parser to read the input file. \section cmdlinemis Miscellaneous \cmdopt{h\, ?} prints the help message. \cmdopt{version} prints version number of Z3. \cmdopt{v:level} be verbose, where is the verbosity level. \cmdopt{nw} disable warning messages. \cmdopt{ini:file} configuration file. Several parameters are available besides the ones listed by \ty{/h}. These parameters can be loaded from an initialization file by using this option. \cmdopt{ini?} display all available INI file parameters. The available \ref config can also be supplied on the command line as a pair parameter-name=parameter-value. \section cmdlineres Resources \cmdopt{T:timeout} set the timeout (in seconds). Setting this option causes the entire process to exit. It is a reliable way to kill Z3. \cmdopt{t:timeout} set the soft timeout (in seconds). It only kills the current query. \cmdopt{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. \section cmdlineout Output \cmdopt{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. \section cmdlinesearch Search heuristics \cmdopt{rs:num} random seed. */