1YICES-SMT(1)                     User Commands                    YICES-SMT(1)
2
3
4

NAME

6       yices-smt - the Yices SMT solver for the SMT-LIB 1.2 language
7

SYNOPSIS

9       yices-smt [ options ] [ file ]
10

DESCRIPTION

12       Runs  the  Yices SMT solver on an input problem written in SMT-LIB 1.2.
13       If no file is given, the problem is read from standard input.
14
15       SMT-LIB 1.2 is the old version of the SMT-LIB language. It was replaced
16       by SMT-LIB 2.0 in 2012.
17

OPTIONS

19       --version, -V
20              Display version and exit.
21
22       --help, -h
23              Display a short help summary.
24
25       --model, -m
26              Print  a  model  (on stdout) if the problem is satisfiable (some
27              variables may be eliminated).
28
29       --full-model, -f
30              Print a full model if the problem  is  satisfiable.  This  gives
31              more details than option --model.
32
33       --verbose, -v
34              Print statistics and other data during the search.
35
36       --stats, -s
37              Print a statistics summary at the end of the search.
38
39       --timeout=timeout,-t timeout
40              Give a timeout in seconds. There is no timeout by default.
41

SEE ALSO

43       yices(1), yices-sat(1), yices-smt2(1)
44
45       For    bug    reporting    and    other   information,   please   visit
46       http://yices.csl.sri.com.
47

AUTHORS

49       Copyright (C) SRI International.
50
51       Yices is developed at  SRI's  Computer  Science  Laboratory.  The  main
52       developers  are  Bruno Dutertre <bruno@csl.sri.com> and Dejan Jovanovic
53       <dejan@csl.sri.com>.
54
55
56
57Yices 2.6.1                      October 2018                     YICES-SMT(1)