(logic QF_AUFBV

 :written_by {Clark Barrett}
 :date {May 7, 2007}
 
 :theory BV_ArraysEx

 :language 
 "Closed quantifier-free formulas built over an arbitrary expansion of the
  BV_ArraysEx signature with free function and predicate symbols over
  the sorts of BV_ArraysEx.  Formulas in ite terms must satisfy the same
  restriction as well, with the exception that they need not be closed (because
  they may be in the scope of a let expression).
 "
 :extensions
 "As in the logic QF_BV."
)