SMT back-end: fix type when RHS will be flattened

When the right-hand side is a member expression the type has to be a bit
vector (unless data types are used).

Author: tautschnig

regression/cbmc/Array_operations1/main.c

@@ -54,6 +54,14 @@ void test_copy()
   __CPROVER_array_copy(array1, array3);
   __CPROVER_assert(array1[10] == 11, "array1[10] is OK");
   __CPROVER_assert(array1[99] == 42, "expected to fail");
+
+  int a[1];
+  struct
+  {
+    int a[1];
+  } s;
+  __CPROVER_array_copy(a, s.a);
+  __CPROVER_assert(a[0] == s.a[0], "array copied");
 }
 
 void test_replace()

src/solvers/smt2/smt2_conv.cpp

@@ -4786,7 +4786,17 @@ void smt2_convt::set_to(const exprt &expr, bool value)
         {
           out << "(define-fun " << smt2_identifier;
           out << " () ";
-          convert_type(equal_expr.lhs().type());
+          if(
+            equal_expr.lhs().type().id() != ID_array ||
+            use_array_theory(prepared_rhs))
+          {
+            convert_type(equal_expr.lhs().type());
+          }
+          else
+          {
+            std::size_t width = boolbv_width(equal_expr.lhs().type());
+            out << "(_ BitVec " << width << ")";
+          }
           out << ' ';
           convert_expr(prepared_rhs);
           out << ')' << '\n';