diff --git a/regression/cbmc/Array_operations1/full-slice.desc b/regression/cbmc/Array_operations1/full-slice.desc
index 9f1f64d8001..7a1611c0d8f 100644
--- a/regression/cbmc/Array_operations1/full-slice.desc
+++ b/regression/cbmc/Array_operations1/full-slice.desc
@@ -10,7 +10,7 @@ main.c
 ^\[test_unequal\.assertion\.4\] .* expected to fail: FAILURE
 ^\[test_unequal\.assertion\.5\] .* expected to fail: FAILURE
 ^\[test_unequal\.assertion\.6\] .* expected to fail: FAILURE
-^\*\* 5 of 14 failed
+^\*\* 5 of 15 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Array_operations1/main.c b/regression/cbmc/Array_operations1/main.c
index a0c7bbc6db8..f4d405bb981 100644
--- a/regression/cbmc/Array_operations1/main.c
+++ b/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()
diff --git a/regression/cbmc/Array_operations1/test.desc b/regression/cbmc/Array_operations1/test.desc
index 9332fb07c38..55311b430f9 100644
--- a/regression/cbmc/Array_operations1/test.desc
+++ b/regression/cbmc/Array_operations1/test.desc
@@ -10,7 +10,7 @@ main.c
 ^\[test_unequal\.assertion\.4\] .* expected to fail: FAILURE
 ^\[test_unequal\.assertion\.5\] .* expected to fail: FAILURE
 ^\[test_unequal\.assertion\.6\] .* expected to fail: FAILURE
-^\*\* 5 of 14 failed
+^\*\* 5 of 15 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index d7806a971b3..3b1a09447a0 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/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';