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

NAME

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

SYNOPSIS

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

DESCRIPTION

12       Z3 [version 4.8.9 - 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       -pp:name
53              display  Z3  parameter  description,  if 'name' is not provided,
54              then all module names are listed.
55
56       -tactics[:name]
57              display built-in  tactics  or  if  argument  is  given,  display
58              detailed information on tactic.
59
60       -probes
61              display avilable probes.
62
63       --     all remaining arguments are assumed to be part of the input file
64              name. This option allows Z3 to read  files  with  strange  names
65              such as: -foo.smt2.
66
67   Resources:
68       -T:timeout
69              set the timeout (in seconds).
70
71       -t:timeout
72              set  the soft timeout (in milli seconds). It only kills the cur‐
73              rent query.
74
75       -memory:Megabytes
76              set a limit for virtual memory consumption.
77
78   Output:
79       -st    display statistics.
80
81       Parameter setting: Global and module parameters can be set in the  com‐
82       mand line.
83
84       param_name=value
85              for setting global parameters.
86
87       module_name.param_name=value
88              for setting module parameters.
89
90       Use 'z3 -p' for the complete list of global and module parameters.
91
92
93
94Z3 version 4.8.9 - 64 bit        December 2020                           Z3(1)