1Z3(1)                            User Commands                           Z3(1)
2
3
4

NAME

6       Z3 - manual page for Z3 version 4.11.2 - 64 bit
7

SYNOPSIS

9       z3 [options] [-file:]file
10

DESCRIPTION

12       Z3 [version 4.11.2 - 64 bit]. (C) Copyright 2006-2016 Microsoft Corp.
13
14   Input format:
15       -smt2  use parser for SMT 2 input format.
16
17       -dl    use parser for Datalog input format.
18
19       -dimacs
20              use parser for DIMACS input format.
21
22       -wcnf  use parser for Weighted CNF DIMACS input format.
23
24       -opb   use parser for PB optimization input format.
25
26       -lp    use parser for a modest subset of CPLEX LP input format.
27
28       -log   use parser for Z3 log input format.
29
30       -in    read formula from standard input.
31
32       -model display model for satisfiable SMT.
33
34   Miscellaneous:
35       -h, -? prints this message.
36
37       -version
38              prints version number of Z3.
39
40       -v:level
41              be verbose, where <level> is the verbosity level.
42
43       -nw    disable warning messages.
44
45       -p     display Z3 global (and module) parameters.
46
47       -pd    display Z3 global (and module) parameter descriptions.
48
49       -pm:name
50              display Z3 module ('name') parameters.
51
52       -pmmd:name
53              display Z3 module ('name') parameters in Markdown format.
54
55       -pp:name
56              display  Z3  parameter  description,  if 'name' is not provided,
57              then all module names are listed.
58
59       -tactics[:name]
60              display built-in tactics or if argument is  given,  display  de‐
61              tailed information on tactic.
62
63       -probes
64              display avilable probes.
65
66       --     all remaining arguments are assumed to be part of the input file
67              name. This option allows Z3 to read  files  with  strange  names
68              such as: -foo.smt2.
69
70   Resources:
71       -T:timeout
72              set the timeout (in seconds).
73
74       -t:timeout
75              set  the soft timeout (in milli seconds). It only kills the cur‐
76              rent query.
77
78       -memory:Megabytes
79              set a limit for virtual memory consumption.
80
81   Output:
82       -st    display statistics.
83
84       Parameter setting: Global and module parameters can be set in the  com‐
85       mand line.
86
87       param_name=value
88              for setting global parameters.
89
90       module_name.param_name=value
91              for setting module parameters.
92
93       Use 'z3 -p' for the complete list of global and module parameters.
94
95
96
97Z3 version 4.11.2 - 64 bit       January 2023                            Z3(1)