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

NAME

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

SYNOPSIS

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

DESCRIPTION

12       Z3 [version 4.12.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       -simplifiers[:name]
64              display  built-in  simplifiers  or if argument is given, display
65              detailed information on simplifier.
66
67       -probes
68              display avilable probes.
69
70       --     all remaining arguments are assumed to be part of the input file
71              name.  This  option  allows  Z3 to read files with strange names
72              such as: -foo.smt2.
73
74   Resources:
75       -T:timeout
76              set the timeout (in seconds).
77
78       -t:timeout
79              set the soft timeout (in milli seconds). It only kills the  cur‐
80              rent query.
81
82       -memory:Megabytes
83              set a limit for virtual memory consumption.
84
85   Output:
86       -st    display statistics.
87
88       Parameter  setting: Global and module parameters can be set in the com‐
89       mand line.
90
91       param_name=value
92              for setting global parameters.
93
94       module_name.param_name=value
95              for setting module parameters.
96
97       Use 'z3 -p' for the complete list of global and module parameters.
98
99
100
101Z3 version 4.12.2 - 64 bit         May 2023                              Z3(1)
Impressum