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

yices-smt - Man Page

the Yices SMT solver for the SMT-LIB 1.2 language


yices-smt [ options ] [ file ]


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

SMT-LIB 1.2 is the old version of the SMT-LIB language. It was replaced by SMT-LIB 2.0 in 2012.


--version,  -V

Display version and exit.

--help,  -h

Display a short help summary.

--model,  -m

Print a model (on stdout) if the problem is satisfiable (some variables may be eliminated).

--full-model,  -f

Print a full model if the problem is satisfiable. This gives more details than option --model.

--verbose,  -v

Print statistics and other data during the search.

--stats,  -s

Print a statistics summary at the end of the search.

--timeout=timeout,-t timeout

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

See Also

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

For bug reporting and other information, 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-smt2(1).

June 2024 Yices 2.6.5