Z3(1)

💖 Z3 — like, the Satisfiability Modulo Theories (SMT) solver 💖

okay bestie, sit down, hydrate, because this is the manual page for Z3(1) and she is that girl. 🫶

---

✨ NAME ✨

Z3 — Satisfiability Modulo Theories (SMT) solver. yeah. that's the whole name. iconic behavior. 👑

---

🌸 SYNOPSIS 🌸

z3 [options] [-file:]file

---

💅 DESCRIPTION 💅

Z3 [version 4.16.0 - 64 bit]. (C) Copyright 2006-2016 Microsoft Corp.

that's her. that's the girl. 64 bit and thriving. ✨

🦋 Input format 🦋

pick your parser, bestie, they're all valid:

• -smt2 — use parser for SMT 2 input format.
• -dl — use parser for Datalog input format.
• -dimacs — use parser for DIMACS input format.
• -wcnf — use parser for Weighted CNF DIMACS input format.
• -opb — use parser for PB optimization input format.
• -lp — use parser for a modest subset of CPLEX LP input format. (modest. she's humble. we love that for her 💜)
• -log — use parser for Z3 log input format.
• -in — read formula from standard input.
• -model — display model for satisfiable SMT.

🎀 Miscellaneous 🎀

the little extras. the garnish. the sprinkles on the algorithm. 🍓

• -h, -? — prints this message.
• -version — prints version number of Z3.
• -v:level — be verbose, where level is the verbosity level. (yes she can be more verbose. she contains multitudes.)
• -nw — disable warning messages.
• -p — display Z3 global (and module) parameters.
• -pd — display Z3 global (and module) parameter descriptions.
• -pm:name — display Z3 module (name) parameters.
• -pmmd:name — display Z3 module (name) parameters in Markdown format. (markdown girlies rise up 📝)
• -pp:name — display Z3 parameter description, if name is not provided, then all module names are listed.
• -tactics[:name] — display built-in tactics or if argument is given, display detailed information on tactic.
• -simplifiers[:name] — display built-in simplifiers or if argument is given, display detailed information on simplifier.
• -probes — display avilable probes.
• -- — all remaining arguments are assumed to be part of the input file name. This option allows Z3 to read files with strange names such as: -foo.smt2.

not the strange filenames 💀 she said "I will handle -foo.smt2 and I will not complain about it." queen.

🌈 Resources 🌈

setting boundaries. very healthy. very main character. 🧚

• -T:timeout — set the timeout (in seconds).
• -t:timeout — set the soft timeout (in milli seconds). It only kills the current query.
• -memory:Megabytes — set a limit for virtual memory consumption.

⭐ Output ⭐

• -st — display statistics.

💜 Parameter setting 💜

Global and module parameters can be set in the command line. yes. directly. in the command line. slay.

• param_name=value — for setting global parameters.
• module_name.param_name=value — for setting module parameters.

Use z3 -p for the complete list of global and module parameters.

---

fr fr, if you're ever lost: run z3 -p and let the parameter list be your guiding light. 🔥

---

and that's the whole page, bestie!! this was Z3 version 4.16.0 - 64 bit, dated March 2026, and it ate. absolutely no crumbs left. periodt. 💅✨🎀🦋