diff --git a/regression/ansi-c/Pointer-to-non-byte/pointer-to-bool.c b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bool.c
new file mode 100644
index 00000000000..1f60e2bbbd6
--- /dev/null
+++ b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bool.c
@@ -0,0 +1,6 @@
+__CPROVER_bool x;
+
+int main()
+{
+  void *p = &x; // should error
+}
diff --git a/regression/ansi-c/Pointer-to-non-byte/pointer-to-bool.desc b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bool.desc
new file mode 100644
index 00000000000..f010c13fb46
--- /dev/null
+++ b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bool.desc
@@ -0,0 +1,7 @@
+CORE
+pointer-to-bool.c
+
+cannot take address of a proper Boolean$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
diff --git a/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array1.c b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array1.c
new file mode 100644
index 00000000000..63dcfd994db
--- /dev/null
+++ b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array1.c
@@ -0,0 +1,6 @@
+__CPROVER_bitvector[123] z[10];
+
+int main()
+{
+  void *p = z; // should error
+}
diff --git a/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array1.desc b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array1.desc
new file mode 100644
index 00000000000..0c4e4de8b23
--- /dev/null
+++ b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array1.desc
@@ -0,0 +1,7 @@
+CORE
+pointer-to-bv-array1.c
+
+bitvector must have width that is a multiple of CHAR_BIT$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
diff --git a/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array2.c b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array2.c
new file mode 100644
index 00000000000..d0479b1d88e
--- /dev/null
+++ b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array2.c
@@ -0,0 +1,6 @@
+__CPROVER_bitvector[123] z[10];
+
+int main()
+{
+  void *p = (int *)z; // should error
+}
diff --git a/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array2.desc b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array2.desc
new file mode 100644
index 00000000000..a6f39c1b88d
--- /dev/null
+++ b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array2.desc
@@ -0,0 +1,7 @@
+CORE
+pointer-to-bv-array2.c
+
+bitvector must have width that is a multiple of CHAR_BIT$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
diff --git a/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv.c b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv.c
new file mode 100644
index 00000000000..8de7bb3be5c
--- /dev/null
+++ b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv.c
@@ -0,0 +1,6 @@
+__CPROVER_bitvector[15] y;
+
+int main()
+{
+  void *p = &y; // should error
+}
diff --git a/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv.desc b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv.desc
new file mode 100644
index 00000000000..ec10cc828f8
--- /dev/null
+++ b/regression/ansi-c/Pointer-to-non-byte/pointer-to-bv.desc
@@ -0,0 +1,7 @@
+CORE
+pointer-to-bv.c
+
+bitvector must have width that is a multiple of CHAR_BIT$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index d4f64ce585f..fe7ea79939d 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -739,6 +739,15 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
 
   if(src_type.id()==ID_array)
   {
+    // This is the promotion from an array
+    // to a pointer to the first element.
+    auto error_opt = check_address_can_be_taken(expr.type());
+    if(error_opt.has_value())
+    {
+      errors.push_back(error_opt.value());
+      return;
+    }
+
     index_exprt index(expr, from_integer(0, c_index_type()));
     expr = typecast_exprt::conditional_cast(address_of_exprt(index), dest_type);
     return;
@@ -765,3 +774,31 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
     }
   }
 }
+
+optionalt<std::string>
+c_typecastt::check_address_can_be_taken(const typet &type)
+{
+  if(type.id() == ID_c_bit_field)
+    return std::string("cannot take address of a bit field");
+
+  if(type.id() == ID_bool)
+    return std::string("cannot take address of a proper Boolean");
+
+  if(can_cast_type<bitvector_typet>(type))
+  {
+    // The width of the bitvector must be a multiple of CHAR_BIT.
+    auto width = to_bitvector_type(type).get_width();
+    if(width % config.ansi_c.char_width != 0)
+    {
+      return std::string(
+        "bitvector must have width that is a multiple of CHAR_BIT");
+    }
+    else
+      return {};
+  }
+
+  if(type.id() == ID_array)
+    return check_address_can_be_taken(to_array_type(type).element_type());
+
+  return {}; // ok
+}
diff --git a/src/ansi-c/c_typecast.h b/src/ansi-c/c_typecast.h
index 7d3525d3c05..3416677a515 100644
--- a/src/ansi-c/c_typecast.h
+++ b/src/ansi-c/c_typecast.h
@@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_ANSI_C_C_TYPECAST_H
 #define CPROVER_ANSI_C_C_TYPECAST_H
 
+#include <util/optional.h>
+
 #include <list>
 #include <string>
 
@@ -65,6 +67,10 @@ class c_typecastt
   std::list<std::string> errors;
   std::list<std::string> warnings;
 
+  /// \return empty when address can be taken,
+  /// error message otherwise
+  static optionalt<std::string> check_address_can_be_taken(const typet &);
+
 protected:
   const namespacet &ns;
 
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index c58ffd8a85d..fb77794081f 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -36,6 +36,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "builtin_factory.h"
 #include "c_expr.h"
 #include "c_qualifiers.h"
+#include "c_typecast.h"
 #include "c_typecheck_base.h"
 #include "expr2c.h"
 #include "padding.h"
@@ -1187,6 +1188,12 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
   }
   else if(op_type.id()==ID_array)
   {
+    // This is the promotion from an array
+    // to a pointer to the first element.
+    auto error_opt = c_typecastt::check_address_can_be_taken(op_type);
+    if(error_opt.has_value())
+      throw invalid_source_file_exceptiont{*error_opt, expr.source_location()};
+
     index_exprt index(op, from_integer(0, c_index_type()));
     op=address_of_exprt(index);
   }
@@ -1710,19 +1717,10 @@ void c_typecheck_baset::typecheck_expr_address_of(exprt &expr)
 {
   exprt &op = to_unary_expr(expr).op();
 
-  if(op.type().id()==ID_c_bit_field)
-  {
-    error().source_location = expr.source_location();
-    error() << "cannot take address of a bit field" << eom;
-    throw 0;
-  }
+  auto error_opt = c_typecastt::check_address_can_be_taken(op.type());
 
-  if(op.is_boolean())
-  {
-    error().source_location = expr.source_location();
-    error() << "cannot take address of a single bit" << eom;
-    throw 0;
-  }
+  if(error_opt.has_value())
+    throw invalid_source_file_exceptiont{*error_opt, expr.source_location()};
 
   // special case: address of label
   if(op.id()==ID_label)