(logic QF_AX

 :written_by {Silvio Ranise and Cesare Tinelli}
 :date {08/04/05}
 
 :theory ArraysEx

 :language 
 "Closed quantifier-free formulas built over an arbitrary expansion of
  the ArraysEx signature with free constant symbols.

  Note that the formulas can contain term (resp., formula) variables 
  as long as they are bound by a let (resp., flet) construct.
  Also, formulas in ite terms must be themselves quantifier-free.
 "
 
)