yices man page

yices ā€” the Yices SMT solver for the Yices language


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


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.


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.


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.

See Also

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

Yices is developed at SRI's Computer Science Laboratory. The main developers are Bruno Dutertre <bruno@csl.sri.com> and Dejan Jovanovic <dejan@csl.sri.com>.

Referenced By

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

June 2017 Yices 2.6.0 User Commands