SMT-LIB Logics (Version 2)

SMT-LIB 2 scripts, which includes all the benchmarks available from the Benchmarks section, refer to one of the following sublogics of the main SMT-LIB logic.

Logic declarations for Version 1.2 of SMT-LIB, now superseded by the ones below, are still available here.

Click on the logic's name to see its declaration in SMT-LIB 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 two-dimentional 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 quantifier-free formulas over the theory of bitvectors and bitvector arrays.

QF_AUFBV:

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

QF_AUFLIA:

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

QF_AX:

Closed quantifier-free formulas over the theory of arrays with extensionality.

QF_BV:

Closed quantifier-free formulas over the theory of fixed-size 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:

Quantifier-free integer arithmetic.

QF_NRA:

Quantifier-free 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 non-linear real arithmetic with uninterpreted sort and function symbols.

UFLRA:

Non-linear real arithmetic with uninterpreted sort and function symbols.

UFNIA:

Non-linear integer arithmetic with uninterpreted sort and function symbols.