\myheading{Theories}

QF\_S -- strings. You may need this to simulate strings to catch bugs like SQL injection.
\url{http://cvc4.cs.stanford.edu/wiki/Strings}.

\begin{lstlisting}
* QF_UF (Uninterpreted Functions): quantifier-free formulas whose
  satisfiability is to be decided modulo the empty theory. Each
  benchmark may introduce its own uninterpreted function and predicate
  symbols.

* QF_IDL (Integer Difference Logic): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of integer
  arithmetic.  The syntax of atomic formulas is restricted to
  difference logic, i.e. x - y op c, where op is either equality or
  inequality and c is an integer constant.

* QF_RDL (Real Difference Logic): this division is like QF_IDL, except
  that the background theory is real arithmetic.

* QF_UFIDL (Integer Difference Logic with Uninterpreted Functions):
  this division contains benchmarks in a logic which is similar to
  QF_IDL, except that it also allows uninterpreted functions and
  predicates.

* QF_LIA (Linear Integer Arithmetic): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of integer
  arithmetic.  The syntax of atomic formulas is restricted to contain
  only linear terms.

* QF_LRA (Linear Real Arithmetic): this division is like QF_LIA,
  except that the background theory is real arithmetic.

* QF_NIA (Nonlinear Integer Arithmetic): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of integer
  arithmetic.  There is no restriction to linear terms.

* QF_UFLIA (Linear Integer Arithmetic with Uninterpreted Functions):
  this division contains benchmarks in a logic which is similar to
  QF_LIA, except that it also allows uninterpreted functions and
  predicates.

* QF_UFLRA (Linear Real Arithmetic with Uninterpreted Functions):
  this division is similar to QF_LRA, except that it also allows
  uninterpreted functions and predicates.

* QF_AX (Arrays with Extensionality): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of arrays which
  includes the extensionality axiom.

* QF_AUFLIA (Linear Integer Arithmetic with Uninterpreted Functions
  and Arrays): quantifier-free formulas to be tested for
  satisfiability modulo a background theory combining linear integer
  arithmetic, uninterpreted function and predicate symbols, and
  extensional arrays.

* QF_BV (Fixed-size Bit-vectors): quantifier-free formulas over bit
  vectors of fixed size.

* QF_AUFBV (Bit-vectors with Arrays and Uninterpreted Functions):
  quantifier-free formulas over bit vectors of fixed size, with arrays
  and uninterpreted functions and predicate symbols.

* AUFLIA+p (Linear Integer Arithmetic with Uninterpreted Functions and
  Arrays, with patterns): quantified formulas to be tested for
  satisfiability modulo a background theory combining linear integer
  arithmetic, uninterpreted function and predicate symbols, and
  extensional arrays. Benchmarks include patterns for guiding
  instantiation mechanisms.

* AUFLIA-p (Linear Integer Arithmetic with Uninterpreted Functions and
  Arrays, without patterns): formulas from AUFLIA+p once all patterns
  have been removed.

* AUFLIRA (Arrays, Uninterpreted Functions, and Linear Arithmetic):
  quantifier formulas with arrays of reals indexed by integers
  (Array1), arrays of Array1 indexed by integers (Array2), and linear
  arithmetic over the integers and reals.

* UFNIA+p (Uninterpreted Functions and Nonlinear Arithmetic, patterns
  included): quantifier formulas with uninterpreted functions and
  nonlinear integer arithmetic.

* AUFNIRA (Arrays, Uninterpreted Functions, and Nonlinear Arithmetic):
  quantifier formulas with arrays of reals indexed by integers
  (Array1), arrays of Array1 indexed by integers (Array2), and
  nonlinear arithmetic over the integers and reals.
\end{lstlisting}

( \href{https://cs.nyu.edu/pipermail/smt-lib/2011/000468.html}{src} )

\lstinputlisting[style=customc,caption=Nicely commented smt\_logic\_codes.h file from Yices]{basics/smt_logic_codes.h}

What is \textit{theory}?

One can say that a SMT solver is a library of various methods on top of a SAT solver.
And sometimes, one \textit{theory}/method can perform better for your problem than another.

You can first start without setting theory explicitly or setting QF\_ALL.
But then you can experiment trying some of them.

It's recommended to set a \textit{theory} that has only features you need, nothing else.

And of course, SMT benchmarks for SMT solvers competition are divided by theories:
\url{http://smt-lib.loria.fr/zip}.