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, now superseded by the ones below, are still available here.

ArraysEx

Functional arrays with extensionality.

Fixed_Size_BitVectors

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.