SMT-LIB Logics

The currently available SMT-LIB benchmarks belong (and refer) to one of the following sublogics of the main SMT-LIB logic.

AUFLIA:

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

AUFLIRA:

Closed linear formulas with free function and predicate symbols over a theory of arrays of 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.

QF_A:

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

QF_AUFBV:

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

QF_AUFLIA:

Closed quantifier-free and linear formulas over the theory of integer arrays with free sort, function and predicate 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 integer linear arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables.

QF_LRA:

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

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 sort, function and predicate symbols.

QF_UFIDL:

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

QF_UFBV:

Unquantified formulas over bitvectors with uninterpreted function and predicate symbols.

QF_UFBV[32] (now deprecated):

Unquantified formulas over bit vectors of size up to 32 bits, with uninterpreted function, and predicate symbols. This logic remains for historical purposes. The preferred logic for current use is now one of QF_BV or QF_UFBV.

QF_UFLIA:

Unquantified integer linear arithmetic with uninterpreted sort, function, and predicate symbols.

QF_UFLRA:

Unquantified real linear arithmetic with uninterpreted sort, function, and predicate symbols.