yices-smt - Man Page
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.
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).