SMTLIB Theories (Version 1)
Note. The theories below are superseded by those defined in Version 2 of SMTLIB.
They are listed here for historical purposes.
Their use is deprecated.
Click on the theory's name for a description of the theory in SMTLIB 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.