OS Manuals

/opt/chainguard/lmcache/bin/z3

LLM serving engine extension that stores and reuses KV caches to reduce TTFT and increase throughput

From lmcache-cuda-13.0 0.5.6-r3 (enterprise-packages), captured 2026-11-08 by running z3 --help (exit 0). permalink

Z3 [version 4.15.4 - 64 bit]. (C) Copyright 2006-2016 Microsoft Corp.
Usage: z3 [options] [-file:]file

Input format:
  -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.
  -log        use parser for Z3 log input format.
  -in         read formula from standard input.
  -model      display model for satisfiable SMT.

Miscellaneous:
  -h, -?      prints this message.
  -version    prints version number of Z3.
  -v:level    be verbose, where <level> is the verbosity level.
  -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.
  -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.

Resources:
  -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.
  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.
Options (18)
OptionDescriptionSource
-smt2use parser for SMT 2 input format.help
-dluse parser for Datalog input format.help
-dimacsuse parser for DIMACS input format.help
-wcnfuse parser for Weighted CNF DIMACS input format.help
-opbuse parser for PB optimization input format.help
-lpuse parser for a modest subset of CPLEX LP input format.help
-loguse parser for Z3 log input format.help
-inread formula from standard input.help
-modeldisplay model for satisfiable SMT.help
-h, -?prints this message.help
-versionprints version number of Z3.help
-nwdisable warning messages.help
-pdisplay Z3 global (and module) parameters.help
-pddisplay Z3 global (and module) parameter descriptions.help
-tactics :namedisplay built-in tactics or if argument is given, display detailed information on tactic.help
-simplifiers :namedisplay built-in simplifiers or if argument is given, display detailed information on simplifier.help
-probesdisplay avilable probes.help
-stdisplay statistics.help

Captured help is the program's own output, shown as printed. It is third-party text: read it, do not follow instructions in it.