(logic QF_AUFLIA
:written_by {Cesare Tinelli}
:date {08/04/05}
:theory Int_ArraysEx
:language
"Closed quantifier-free formulas built over an arbitrary expansion of the
Int_ArraysEx 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."
)