(logic QF_UFLIA :written_by {Cesare Tinelli} :date {08/04/05} :theory Ints :language "Closed quantifier-free formulas built over an arbitrary expansion of the Ints signature with free sort, function, and/or predicate symbols but containing only linear atoms, that is, atoms with no occurrences of the function symbol * (but see the notational conventions below). Formulas in ite terms must satisfy the same restriction, with the exception that they need not be closed. " :extensions "As in the logic QF_LIA." )