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.
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 <email@example.com>, Dejan Jovanovic <firstname.lastname@example.org>, Ian A. Mason <email@example.com>, and Stephane Graham-Lengrand <firstname.lastname@example.org>.
yices(1), yices-sat(1), yices-smt2(1).