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

NAME

6       yices-smt2 - the Yices SMT solver for the SMT-LIB 2 language
7

SYNOPSIS

9       yices-smt2 [ option ] [ file ]
10

DESCRIPTION

12       Runs the Yices SMT solver on an input problem written in SMT-LIB 2 lan‐
13       guage.  If no file is given, the problem is read from standard input.
14
15       The  SMT-LIB  language  and  logical   theories   are   documented   at
16       http://smtlib.cs.uiowa.edu.
17

OPTIONS

19       --version, -V
20              Display version and exit.
21
22       --help, -h
23              Display a short help summary.
24
25       --verbosity=level, -v level
26              Set the verbosity level (default = 0).
27
28       --timeout=timeout,-t timeout
29              Give a timeout in seconds. There is no timeout by default.
30
31       --stats, -s
32              Print a statistics summary before exiting.
33
34       --incremental
35              Enable support for the push/pop commands.
36
37       --interactive
38              Run in interactive mode.
39
40              This  option is ignored if an input file is given on the command
41              line. Otherwise, yices-smt2 prints a prompt  before  every  com‐
42              mand. This also sets the SMT-LIB option :print-success to true.
43

SEE ALSO

45       yices(1), yices-sat(1), yices-smt(1),
46
47       To  report  bugs  and  to  get  the  full  documentation,  please visit
48       http://yices.csl.sri.com.
49

AUTHORS

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