Revert "array expressions suppress SMT simplification in non-array logics"

This reverts commit 1100fae5. It turns out that
some SMT solvers don't stick to the constraints of the logic and happily accept
expressions outside of it. So we would like to still emit things that may be
outside the given logic in case the solver understands them.

The particular situation that motivated this is that Z3 does not understand the
logic QF_ALIA and falls back to its behaviour of accepting a superset of the
logics it knows. This means that, e.g., switching from QF_ALIA to QF_AUFLIA
makes some problems unsolvable because Z3 *does* know QF_AUFLIA and imposes
further restrictions.