(logic AUFLIA2

 ; based on Cesare Tinelli's AUFLIA logic
 :written_by {Michal Moskal}
 :date {04/01/07}
 
 :theory Int_Heaps

 :language 
 "Closed formulas built over an arbitrary expansion of the
  Int_Heaps 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."
)