Decision Procedures for Extensions of the Theory of Arrays