SMT2 back-end: do not flatten flattened arrays

convert_expr may flatten an array anyway, in which case flatten_array
would generate select statements over bitvectors instead of arrays (as
flatten_array itself invokes convert_expr to supposedly construct the
array expression).

Author: tautschnig

regression/cbmc/Array_operations2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^\[main.assertion.12\] line 34 assertion arr\[1\].c\[2\] == 0: FAILURE$

src/solvers/smt2/smt2_conv.cpp

@@ -3060,7 +3060,7 @@ void smt2_convt::convert_struct(const struct_exprt &expr)
         exprt op=expr.operands()[i-1];
 
         // may need to flatten array-theory arrays in there
-        if(op.type().id() == ID_array)
+        if(op.type().id() == ID_array && use_array_theory(op))
           flatten_array(op);
         else if(op.type().id() == ID_bool)
           flatten2bv(op);