yices - Man Page

yices [ options ] [ file ]

Runs the Yices SMT solver. The input must be in the Yices specification language. If no file is given, Yices reads commands from standard input.

--version,  -V

Display version and exit.

--help,  -h

Display a short help summary.

--verbosity=level, -v level

Set the verbosity level (default = 0).

--logic=name

Configure Yices for a specific logic.

The name must be either an SMT-LIB logic name (e.g., QF_UFLIA) or the special symbol NONE to select propositional logic.

--arith-solver=solver

Select the arithmetic solver.

The solver may be either simplex or floyd-warshall or auto. This option is ignored unless the logic is either QF_RDL or QF_IDL.

--mode=mode

Select the usage mode.

The mode maybe one-shot or multi-checks or interactive or push-pop or ef.

• one-shot: only one call to (check) is allowed. No assertions are allowed after (check). Commands (push) and (pop) are not supported.
• multi-checks: several calls (check) are allowed. Adding assertions after check is allowed. Commands (push) and (pop) are not supported.
• push-pop: like multi-check but with support for (push) and (pop).
• interactive: like push-pop. In addition, Yices restores the context to a clean state if (check) is interrupted.
• ef: enable the exist-forall solver, that is, command (ef-solve) can be used. This is like one-shot in that only one call to (ef-solve) is allowed.

The default mode is push-pop.

--mcsat

Force use of the MCSAT solver.

--print-success

Print ok after every command that would otherwise execute silently.

yices-sat(1), yices-smt(1), yices-smt2(1)

To report bugs and to get the full documentation, please visit http://yices.csl.sri.com.

Copyright (C) SRI International.

Yices is developed at SRI's Computer Science Laboratory. The main developers are Bruno Dutertre <bruno@csl.sri.com>, Dejan Jovanovic <dejan@csl.sri.com>, Ian A. Mason <iam@csl.sri.com>, and Stephane Graham-Lengrand <stephane.graham-lengrand@sri.com>.

yices-sat(1), yices-smt(1), yices-smt2(1).