yices-smt2 man page

yices-smt2 ā€” the Yices SMT solver for the SMT-LIB 2 language


yices-smt2 [ option ] [ file ]


Runs the Yices SMT solver on an input problem written in SMT-LIB 2 language. If no file is given, the problem is read from standard input.

The SMT-LIB language and logical theories are documented at http://smtlib.cs.uiowa.edu.


--version, -V

Display version and exit.

--help, -h

Display a short help summary.

--verbosity=level, -v level

Set the verbosity level (default = 0).

--timeout=timeout,-t timeout

Give a timeout in seconds. There is no timeout by default.

--stats, -s

Print a statistics summary before exiting.


Enable support for the push/pop commands.


Run in interactive mode.

This option is ignored if an input file is given on the command line. Otherwise, yices-smt2 prints a prompt before every command. This also sets the SMT-LIB option :print-success to true.

See Also

yices(1), yices-sat(1), yices-smt(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).

June 2017 Yices 2.6.0 User Commands