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). Also, make sure the same flattening logic applies to
1-element structs.

Author: tautschnig

regression/cbmc/array-function-parameters/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 test.c
 --function test --min-null-tree-depth 2 --max-nondet-tree-depth 2 --bounds-check
 ^EXIT=10$

src/solvers/smt2/smt2_conv.cpp

@@ -3142,7 +3142,16 @@ void smt2_convt::convert_struct(const struct_exprt &expr)
   else
   {
     if(components.size()==1)
-      convert_expr(expr.op0());
+    {
+      const exprt &op = expr.op0();
+      // may need to flatten array-theory arrays in there
+      if(op.type().id() == ID_array && use_array_theory(op))
+        flatten_array(op);
+      else if(op.type().id() == ID_bool)
+        flatten2bv(op);
+      else
+        convert_expr(op);
+    }
     else
     {
       // SMT-LIB 2 concat is binary only
@@ -3153,7 +3162,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);