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:
Linear real arithmetic with uninterpreted sort and function symbols.

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