(logic QF_AX
:written_by {Silvio Ranise and Cesare Tinelli}
:date {08/04/05}
:theory ArraysEx
:language
"Closed quantifier-free formulas built over an arbitrary expansion of
the ArraysEx signature with free constant symbols.
Note that the formulas can contain term (resp., formula) variables
as long as they are bound by a let (resp., flet) construct.
Also, formulas in ite terms must be themselves quantifier-free.
"
)