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

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);