(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."
)