z3 - Online in the Cloud

PROGRAM:

NAME

z3 - a state-of-the art theorem prover from Microsoft Research

SYNOPSIS

z3 [options] [-file:]file

DESCRIPTION

This manual page documents briefly the z3 command.

z3 Z3 is a state-of-the art theorem prover from Microsoft Research. It can be used to
check the satisfiability of logical formulas over one or more theories. Z3 offers a
compelling match for software analysis and verification tools, since several common
software constructs map directly into supported theories.

Input format

-smt Use parser for SMT input format.

-smt2 Use parser for SMT 2 input format.

-dl Use parser for Datalog input format.

-dimacs
Use parser for DIMACS input format.

-log Use parser for Z3 log input format.

-in Read formula from standard input.

Miscellaneous

-h | -?
Prints the usage information.

-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.

-pp:name
Display Z3 parameter description, if <name> is not provided, then all module names
are listed.

-- 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. Use 'z3 -p' for the complete
list of global and module parameters.

param_name=value
For setting global parameters.

module_name.param_name=value
For setting module parameters.

Use z3 online using onworks.net services