SMTLIB Logics (Version 2)
SMTLIB 2 scripts, which includes all the benchmarks available from the Benchmarks section, refer to one of the following sublogics of the main SMTLIB logic.
Logic declarations for Version 1.2 of SMTLIB, now superseded by the ones below, are still available here.
Click on the logic's name to see its declaration in SMTLIB format.

AUFLIA:

Closed formulas over the theory of linear integer arithmetic and arrays
extended with free sort and function symbols
but restricted to arrays with integer indices and values.

AUFLIRA:

Closed linear formulas with free sort and function symbols
over one and twodimentional arrays of integer index and real value.

AUFNIRA:

Closed formulas with free function and predicate symbols
over a theory of arrays of arrays of integer index and real value.

LRA:

Closed linear formulas in linear real arithmetic.

QF_ABV:

Closed quantifierfree formulas over the theory of bitvectors and bitvector arrays.

QF_AUFBV:

Closed quantifierfree formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols.

QF_AUFLIA:

Closed quantifierfree linear formulas over the theory of integer arrays
extended with free sort and function symbols.

QF_AX:

Closed quantifierfree formulas over the theory of arrays with extensionality.

QF_BV:

Closed quantifierfree formulas over the theory of fixedsize bitvectors.

QF_IDL:

Difference Logic over the integers.
In essence,
Boolean combinations of inequations of the form x  y < b
where x and y are integer variables and b is an integer constant.

QF_LIA:

Unquantified linear integer arithmetic.
In essence,
Boolean combinations of inequations between
linear polynomials over integer variables.

QF_LRA:

Unquantified linear real arithmetic.
In essence,
Boolean combinations of inequations between linear polynomials
over real variables.

QF_NIA:

Quantifierfree integer arithmetic.

QF_NRA:

Quantifierfree real arithmetic.

QF_RDL:

Difference Logic over the reals.
In essence,
Boolean combinations of inequations of the form x  y < b
where x and y are real variables and b is a rational constant.

QF_UF:

Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols.

QF_UFBV:

Unquantified formulas over bitvectors with uninterpreted sort function and symbols.

QF_UFIDL:

Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols.

QF_UFLIA:

Unquantified linear integer arithmetic with uninterpreted sort and function symbols.

QF_UFLRA:

Unquantified linear real arithmetic with uninterpreted sort and function symbols.

QF_UFNRA:

Unquantified nonlinear real arithmetic with uninterpreted sort and function symbols.

UFLRA:

Linear real arithmetic with uninterpreted sort and function symbols.

UFNIA:

Nonlinear integer arithmetic with uninterpreted sort and function symbols.