# SMT Logics

The following table lists the names of all the official SMT-LIB logics at http://smt-lib.org (as of January 2015) and indicates whether Yices supports them. Currently, Yices supports most quantifier-free SMT-LIB logics. Nonlinear real arithmetic is supported by using the MCSAT solver of Yices.

Logic name Description Supported ALIA Arrays, Linear Integer Arithmetic, Quantifiers No AUFLIA Arrays, Uninterpreted Functions, Linear Integer Arithmetic, Quantifiers No AUFLIRA Arrays, Uninterpreted Functions, Mixed Linear Arithmetic, Quantifiers No AUFNIRA Arrays, Uninterpreted Functions, Mixed Nonlinear Arithmetic, Quantifiers No LIA Linear Integer Arithmetic, Quantifiers No LRA Linear Real Arithmetic, Quantifiers No NIA Nonlinear Integer Arithmetic, Quantifiers No NRA Nonlinear Real Arithmetic, Quantifiers No QF_ABV Arrays and Bitvectors Yes QF_ALIA Arrays and Linear Integer Arithmetic Yes QF_AUFBV Arrays, Uninterpreted Functions, and Bitvectors Yes QF_AUFLIA Arrays, Uninterpreted Functions, and Linear Integer Arithmetic Yes QF_AX Arrays (with extensionality) Yes QF_BV Bitvectors Yes QF_IDL Integer Difference Logic Yes QF_LIA Linear Integer Arithmetic Yes QF_LRA Linear Real Arithmetic Yes QF_NIA Nonlinear Integer Arithmetic Yes QF_NIRA Mixed Nonlinear Arithmetic Yes QF_NRA Nonlinear Real Arithmetic Yes QF_RDL Real Difference Logic Yes QF_UF Uninterpreted Functions Yes QF_UFBV Uninterpreted Functions and Bitvectors Yes QF_UFIDL Uninterpreted Functions and Integer Difference Logic Yes QF_UFLIA Uninterpreted Functions and Linear Integer Arithmetic Yes QF_UFLRA Uninterpreted Functions and Linear Real Arithmetic Yes QF_UFNIA Uninterpreted Functions and Nonlinear Integer Arithmetic Yes QF_UFNIRA Uninterpreted Functions and Mixed Nonlinear Arithmetic Yes QF_UFNRA Uninterpreted Functions and Nonlinear Real Arithmetic Yes UFLRA Uninterpreted Functions, Linear Real Arithmetic, Quantifiers No UFNIA Uninterpreted Functions, Nonlinear Integer Arithmetic, Quantifiers No

Yices also recognizes and supports some logic names that are not officially part of SMT-LIB.

Logic name Description QF_ALRA Arrays and Linear Real Arithmetic QF_ALIRA Arrays and Mixed Linear Arithmetic QF_AUF Arrays and Uninterpreted Functions QF_AUFLRA Arrays, Uninterpreted Functions, Linear Real Arithmetic QF_AUFLIRA Arrays, Uninterpreted Functions, Mixed Linear Arithmetic QF_LIRA Mixed Linear Arithmetic QF_UFLIRA Uninterpreted Functions and Mixed Linear Arithmetic QF_UFRDL Uninterpreted Functions and Real Difference Logic