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.
Force use of the MCSAT solver.
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 <firstname.lastname@example.org>, Dejan Jovanovic <email@example.com>, Ian A. Mason <firstname.lastname@example.org>, and Stephane Graham-Lengrand <email@example.com>.
yices-sat(1), yices-smt(1), yices-smt2(1).