yices-smt2 - Man Page

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.

--incremental

Enable support for the push/pop commands.

--interactive

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.

--mcsat

Force use of the MCSAT solver.

--smt2-model-format

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

--bvconst-in-decimal

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

--delegate=solver

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.

--dimacs=filename

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

--mcsat-help

Display options used only by the MCSAT solver.

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

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