(logic AUFLIA

 :written_by {Cesare Tinelli}
 :date {12/04/05}
 
 :theory Int_ArraysEx

 :language 
 "Closed 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."
)