blob: bc055c35469d37f71ab0495dfbdfbf931f3d6bad (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(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."
)
|
