diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.class b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.class
new file mode 100644
index 00000000000..1811bee9941
Binary files /dev/null and b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.class differ
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.java b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.java
new file mode 100644
index 00000000000..b8ae6fca5b6
--- /dev/null
+++ b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.java
@@ -0,0 +1,11 @@
+public class Test {
+  public static void check(Integer t) {
+    if (t != null)
+      try {
+        Integer[] arr = new Integer[-7];
+        assert false;
+      } catch (NegativeArraySizeException e) {
+        assert false;
+      }
+  }
+}
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/test.desc b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/test.desc
new file mode 100644
index 00000000000..306126c0dae
--- /dev/null
+++ b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/test.desc
@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.check
+line 5 Array size should be >= 0: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that defining an array with negative size does not crash JBMC
diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp
index 0e5cbd09c14..45ff8d99151 100644
--- a/src/goto-symex/field_sensitivity.cpp
+++ b/src/goto-symex/field_sensitivity.cpp
@@ -180,14 +180,15 @@ exprt field_sensitivityt::get_fields(
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(
     ssa_expr.type().id() == ID_array &&
-    to_array_type(ssa_expr.type()).size().id() == ID_constant &&
-    numeric_cast_v<mp_integer>(
-      to_constant_expr(to_array_type(ssa_expr.type()).size())) <=
-      max_field_sensitivity_array_size)
+    to_array_type(ssa_expr.type()).size().id() == ID_constant)
   {
+    const mp_integer mp_array_size = numeric_cast_v<mp_integer>(
+      to_constant_expr(to_array_type(ssa_expr.type()).size()));
+    if(mp_array_size < 0 || mp_array_size > max_field_sensitivity_array_size)
+      return ssa_expr;
+
     const array_typet &type = to_array_type(ssa_expr.type());
-    const std::size_t array_size =
-      numeric_cast_v<std::size_t>(to_constant_expr(type.size()));
+    const std::size_t array_size = numeric_cast_v<std::size_t>(mp_array_size);
 
     array_exprt result(type);
     result.reserve_operands(array_size);
diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp
index ba7c66af987..57c5bc3e3cd 100644
--- a/src/solvers/flattening/boolbv_width.cpp
+++ b/src/solvers/flattening/boolbv_width.cpp
@@ -141,7 +141,10 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
       if(total>(1<<30)) // realistic limit
         throw analysis_exceptiont("array too large for flattening");
 
-      entry.total_width = numeric_cast_v<std::size_t>(total);
+      if(total < 0)
+        entry.total_width = 0;
+      else
+        entry.total_width = numeric_cast_v<std::size_t>(total);
     }
   }
   else if(type_id==ID_vector)