Word-level model checking is a problem of deciding whether all reachable states of the given symbolic transition system with bit-vector state variables satisfy the given property. The symbolic transition system consists of first-order formulas over bit-vector logic that describe the set of initial states and the transition relation. It has been shown that the problem is PSPACE-complete if the bit-widths and constants in the formulas are encoded in unary and EXPSPACE-complete if the bit-widths and constants are encoded in binary. In practice, the systems contain not only registers that are modeled by bit-vector variables, but also memories that are modeled as arrays. This generalizes the problem to model checking of systems described by formulas over the theory of bit-vectors and arrays. The computational complexity of this problem is currently unknown. The student will identify and prove the complexity class of the problem or identify a practically significant syntactic fragment of the systems for which the complexity can be provided and proven.