(logic QF_UF
:smt-lib-version 2.6
:smt-lib-release "2017-11-24"
:written-by "Cesare Tinelli"
:date "2010-04-14"
:last-updated "2015-04-25"
:update-history
"Note: history only accounts for content changes, not release changes.
2015-04-25 Updated to Version 2.5.
"
:theories () ; includes just Core theory
:language
"Closed quantifier-free formulas built over an arbitrary expansion of
the Core signature with free sort and function symbols.
"
:values
"For each sort other than Bool the set of values is abstract.
For Bool it is defined as in the Core theory declaration.
"
:notes
"Formulas can contain variables as long as they are bound by a let binder.
"
:notes
"All the free symbols used in scripts for this logic must be declared in
the scripts themselves.
"
)
