yices-smt man page

yices-smt ā€” the Yices SMT solver for the SMT-LIB 1.2 language

Synopsis

yices-smt [ options ] [ file ]

Description

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.

Options

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

Authors

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

June 2017 Yices 2.6.0 User Commands