Your company here — click to reach over 10,000 unique daily visitors

yices-smt2 - Man Page

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.


Force use of the MCSAT solver.


Print models in the SMT-LIB format (instead of the default Yices format)..


Print bitvector constants using the SMT-LIB decimal format, instead of the binary format.


Selects an third-party backend SAT solver for bit-vector problems.

The solver must be either cadical or cryptominisat or y2sat. This option has no effect unless the logic if QF_BV.


Bit-blast then export the CNF to a file in the DIMACS format. This option is ignored unless the logic is QF_BV.


Display options used only by the MCSAT solver.

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.

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

Referenced By

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

October 2021 Yices 2.6.4