(logic QF_AX

 :smt-lib-version 2.0
 :written_by "Cesare Tinelli"
 :date "2010-04-30"
 
 :theories (ArraysEx)
 
 :language 
 "Closed quantifier-free formulas built over an arbitrary expansion of
  the ArraysEx signature with free sort and constant symbols.
 "

 :notes
 "Formulas can contain variables as long as they are bound by a let binder."
 
)