Add original test case as a regression test in ansi-c/ folder.

Author: NlightNFotis

regression/ansi-c/Issue_7104_Bv_Size/deref.c

@@ -0,0 +1,18 @@
+struct Foo1
+{
+  __CPROVER_bitvector[1] m_array[2];
+};
+struct Foo8
+{
+  __CPROVER_bitvector[8] m_array[2];
+};
+
+int main(void)
+{
+  struct Foo1 f1;
+  struct Foo8 f8;
+
+  __CPROVER_assert(f1.m_array[1] == *(f1.m_array + 1), "");
+  __CPROVER_assert(f8.m_array[1] == *(f8.m_array + 1), "");
+  return 0;
+}

regression/ansi-c/Issue_7104_Bv_Size/deref.desc

@@ -0,0 +1,13 @@
+CORE
+deref.c
+
+^EXIT=1$
+^SIGNAL=0$
+only bitvectors of size multiple of 8 can be dereferenced
+^CONVERSION ERROR$
+--
+--
+This is checking that dereferenced __CPROVER_bitvectors always have a size
+that is a multiple of 8.
+
+For more information, please have a look at https://github.com/diffblue/cbmc/issues/7104