array expressions suppress SMT simplification in non-array logics

When using an SMT logic like QF_LIA (`--smt-logic QF_LIA`) with no support for
arrays, the SMT bridge would translate models containing array expressions. This
meant the SMT solver would receive a problem it would not understand. We now
bail out of translation when encountering an array expression while using a
logic that does not support arrays.