diff --git a/regression/cbmc/Array_UF21/main.c b/regression/cbmc/Array_UF21/main.c
new file mode 100644
index 00000000000..e2a99771004
--- /dev/null
+++ b/regression/cbmc/Array_UF21/main.c
@@ -0,0 +1,6 @@
+int main()
+{
+  int x[0] = {};
+  int a = x[-1];
+  x[a] = 42;
+}
diff --git a/regression/cbmc/Array_UF21/test.desc b/regression/cbmc/Array_UF21/test.desc
new file mode 100644
index 00000000000..e9d3c4ebe15
--- /dev/null
+++ b/regression/cbmc/Array_UF21/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--arrays-uf-always --bounds-check
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Invariant check failed
diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index 111a627e919..0fdd83ec127 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -715,13 +715,13 @@ void arrayst::add_array_constraints_array_constant(
       // We have a constant index - just pick the element at that index from the
       // array constant.
 
-      const std::size_t i =
-        numeric_cast_v<std::size_t>(to_constant_expr(index));
+      const optionalt<std::size_t> i =
+        numeric_cast<std::size_t>(to_constant_expr(index));
       // if the access is out of bounds, we leave it unconstrained
-      if(i >= operands.size())
+      if(!i.has_value() || *i >= operands.size())
         continue;
 
-      const exprt v = operands[i];
+      const exprt v = operands[*i];
       DATA_INVARIANT(
         index_expr.type() == v.type(),
         "array operand type should match array element type");