(logic QF_UFBV

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

:theory Fixed_Size_BitVectors

:language
 "Closed quantifier-free formulas built over an arbitrary expansion of the
  Fixed_Size_BitVectors signature with free function and predicate symbols over
  the sorts BitVec[m] for 0 < m.  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."
)