A simple theory of arrays is obtained if we simply allow function update expressions in FOL, as in FOL with Update Expressions. As we explained there, this theory can be reduced to FOL. The reduction does not introduce quantifiers, so we obtain decidability for quantifier-free theory of arrays.

• Calculus of Computation Textbook Section 9.5
• The UCLID Decision Procedure