SMT-LIB Theories (Version 1)

Note. The theories below are superseded by those defined in Version 2 of SMT-LIB. They are listed here for historical purposes. Their use is deprecated.

Click on the theory's name for a description of the theory in SMT-LIB format.

Arrays

Functional arrays without extensionality.

ArraysEx

Functional arrays with extensionality.

Fixed_Size_BitVectors[32]

Bit vectors with size up to 32 bits.

Fixed_Size_BitVectors

Bit vectors with arbitrary size.

BitVector_ArraysEx

Bit vectors with arbitrary size, plus arrays indexed by and containing bit vectors.

Empty

Empty theory over the empty signature.

Ints

Integer numbers.

Int_Arrays

Arrays of integer index and value.

Int_ArraysEx

Arrays of integer index and value with extensionality axiom.

Int_Int_Real_Array_ArraysEx

Arrays of arrays of integer index and real value, with extensionality axiom.

Reals

Real numbers.

Reals_Ints

Real and integer numbers.