SMT-LIB Theories (Version 2)

Click on the theory's name to see its declaration in Version 2 of the SMT-LIB format.

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

ArraysEx
Functional arrays with extensionality.

FixedSizeBitVectors
Bit vectors with arbitrary size.

Core
Core theory, defining the basic Boolean operators.

Ints
Integer numbers.

Reals
Real numbers.

Reals_Ints
Real and integer numbers.