Merge pull request #7252 from tautschnig/bugfixes/array-lhs

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

Author: tautschnig

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

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

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

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