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
44       --mcsat
45              Force use of the MCSAT solver.
46
47       --smt2-model-format
48              Print models in the SMT-LIB format (instead of the default Yices
49              format)..
50
51       --bvconst-in-decimal
52              Print bitvector constants using the SMT-LIB decimal format,  in‐
53              stead of the binary format.
54
55       --delegate=solver
56              Selects  an  third-party backend SAT solver for bit-vector prob‐
57              lems.
58
59              The solver must be either cadical  or  cryptominisat  or  y2sat.
60              This option has no effect unless the logic if QF_BV.
61
62       --dimacs=filename
63              Bit-blast  then  export  the CNF to a file in the DIMACS format.
64              This option is ignored unless the logic is QF_BV.
65
66       --mcsat-help
67              Display options used only by the MCSAT solver.
68

SEE ALSO

70       yices(1), yices-sat(1), yices-smt(1),
71
72       To report  bugs  and  to  get  the  full  documentation,  please  visit
73       http://yices.csl.sri.com.
74

AUTHORS

76       Copyright (C) SRI International.
77
78       Yices  is  developed at SRI's Computer Science Laboratory. The main de‐
79       velopers are Bruno Dutertre <bruno@csl.sri.com>, Dejan  Jovanovic  <de‐
80       jan@csl.sri.com>,  Ian A. Mason <iam@csl.sri.com>, and Stephane Graham-
81       Lengrand <stephane.graham-lengrand@sri.com>.
82
83
84
85Yices 2.6.4                      October 2021                    YICES-SMT2(1)
Impressum