SMT-LIB logics refer to one or more theories below. Click on a theory's name to see its declaration in Version 2.x of the format.
- Functional arrays with extensionality
- Bit vectors with arbitrary size
- Core theory, defining the basic Boolean operators
- Floating point numbers
- Integer numbers
- Real numbers
- Real and integer numbers
Theory declarations for Version 1.2 of SMT-LIB, superseded by the ones above, are still available here although their use is deprecated.