  We prove an NP upper bound on a theory of integer-indexed integer-valued
arrays that extends combinatory array logic with an ordering relation on the
index set and the ability to express sums of elements. We compare our fragment
with seven other fragments in the literature in terms of their expressiveness
and computational complexity.
