(logic QF_UFBV

:smt-lib-version 2.0
:written_by "Cesare Tinelli"
:date "2011-06-11"

:theories ( Fixed_Size_BitVectors )

:language
"Closed quantifier-free formulas built over arbitrary expansions of
 the Fixed_Size_BitVectors signature with free sort and function
 symbols.
"

:extensions
"As in the logic QF_BV."
)