diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/Test.class b/jbmc/regression/jbmc/array-cell-sensitivity1/Test.class
new file mode 100644
index 00000000000..57c9912d571
Binary files /dev/null and b/jbmc/regression/jbmc/array-cell-sensitivity1/Test.class differ
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/Test.java b/jbmc/regression/jbmc/array-cell-sensitivity1/Test.java
new file mode 100644
index 00000000000..dacca2ec6fc
--- /dev/null
+++ b/jbmc/regression/jbmc/array-cell-sensitivity1/Test.java
@@ -0,0 +1,10 @@
+public class Test {
+
+  public static void main(int unknown) {
+
+    int[] x = new int[10];
+    x[unknown] = 1;
+    x[1] = unknown;
+    assert (x[1] == unknown);
+  }
+}
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc
new file mode 100644
index 00000000000..9526f00fcb0
--- /dev/null
+++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc
@@ -0,0 +1,20 @@
+CORE
+Test.class
+--function Test.main --show-vcc --max-field-sensitivity-array-size 10
+symex_dynamic::dynamic_2_array#2\[\[0\]\] = symex_dynamic::dynamic_2_array#2\[0\]
+symex_dynamic::dynamic_2_array#2\[\[1\]\] = symex_dynamic::dynamic_2_array#2\[1\]
+symex_dynamic::dynamic_2_array#2\[\[2\]\] = symex_dynamic::dynamic_2_array#2\[2\]
+symex_dynamic::dynamic_2_array#2\[\[3\]\] = symex_dynamic::dynamic_2_array#2\[3\]
+symex_dynamic::dynamic_2_array#2\[\[4\]\] = symex_dynamic::dynamic_2_array#2\[4\]
+symex_dynamic::dynamic_2_array#2\[\[5\]\] = symex_dynamic::dynamic_2_array#2\[5\]
+symex_dynamic::dynamic_2_array#2\[\[6\]\] = symex_dynamic::dynamic_2_array#2\[6\]
+symex_dynamic::dynamic_2_array#2\[\[7\]\] = symex_dynamic::dynamic_2_array#2\[7\]
+symex_dynamic::dynamic_2_array#2\[\[8\]\] = symex_dynamic::dynamic_2_array#2\[8\]
+symex_dynamic::dynamic_2_array#2\[\[9\]\] = symex_dynamic::dynamic_2_array#2\[9\]
+symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This checks that field sensitvity is still applied to an array of size 10
+when the max is set to 10.
\ No newline at end of file
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc
new file mode 100644
index 00000000000..1ebf5798464
--- /dev/null
+++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc
@@ -0,0 +1,11 @@
+CORE
+Test.class
+--function Test.main --show-vcc --max-field-sensitivity-array-size 9
+^EXIT=0$
+^SIGNAL=0$
+symex_dynamic::dynamic_2_array#[0-9]\[1\]
+--
+symex_dynamic::dynamic_2_array#[0-9]\[\[[0-9]\]\]
+--
+This checks that field sensitvity is not applied to an array of size 10
+when the max is set to 9.
\ No newline at end of file
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc
new file mode 100644
index 00000000000..fbc5a83f0f5
--- /dev/null
+++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc
@@ -0,0 +1,11 @@
+CORE
+Test.class
+--function Test.main --show-vcc --no-array-field-sensitivity
+^EXIT=0$
+^SIGNAL=0$
+symex_dynamic::dynamic_2_array#[0-9]\[1\]
+--
+symex_dynamic::dynamic_2_array#[0-9]\[\[[0-9]\]\]
+--
+This checks that field sensitvity is not applied to arrays when
+no-array-field-sensitivity is used.
\ No newline at end of file
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc
new file mode 100644
index 00000000000..25c7ce03e0e
--- /dev/null
+++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc
@@ -0,0 +1,22 @@
+CORE
+Test.class
+--function Test.main --show-vcc
+symex_dynamic::dynamic_2_array#2\[\[0\]\] = symex_dynamic::dynamic_2_array#2\[0\]
+symex_dynamic::dynamic_2_array#2\[\[1\]\] = symex_dynamic::dynamic_2_array#2\[1\]
+symex_dynamic::dynamic_2_array#2\[\[2\]\] = symex_dynamic::dynamic_2_array#2\[2\]
+symex_dynamic::dynamic_2_array#2\[\[3\]\] = symex_dynamic::dynamic_2_array#2\[3\]
+symex_dynamic::dynamic_2_array#2\[\[4\]\] = symex_dynamic::dynamic_2_array#2\[4\]
+symex_dynamic::dynamic_2_array#2\[\[5\]\] = symex_dynamic::dynamic_2_array#2\[5\]
+symex_dynamic::dynamic_2_array#2\[\[6\]\] = symex_dynamic::dynamic_2_array#2\[6\]
+symex_dynamic::dynamic_2_array#2\[\[7\]\] = symex_dynamic::dynamic_2_array#2\[7\]
+symex_dynamic::dynamic_2_array#2\[\[8\]\] = symex_dynamic::dynamic_2_array#2\[8\]
+symex_dynamic::dynamic_2_array#2\[\[9\]\] = symex_dynamic::dynamic_2_array#2\[9\]
+symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
+^EXIT=0$
+^SIGNAL=0$
+--
+symex_dynamic::dynamic_2_array#3\[\[[023456789]\]\] =
+--
+This checks that a write to a Java array with an unknown index uses a whole-array
+write followed by array-cell expansion, but one targeting a constant index uses
+a single-cell symbol without expansion.
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/Test.class b/jbmc/regression/jbmc/array-cell-sensitivity2/Test.class
new file mode 100644
index 00000000000..ae3d24793dc
Binary files /dev/null and b/jbmc/regression/jbmc/array-cell-sensitivity2/Test.class differ
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/Test.java b/jbmc/regression/jbmc/array-cell-sensitivity2/Test.java
new file mode 100644
index 00000000000..b58d9705aaf
--- /dev/null
+++ b/jbmc/regression/jbmc/array-cell-sensitivity2/Test.java
@@ -0,0 +1,21 @@
+public class Test {
+
+  public int data;
+  public Test[] children = new Test[2];
+
+  public static void main(int unknown) {
+
+    Test[] root = new Test[2];
+    Test node1 = new Test();
+    Test node2 = new Test();
+    root[0] = node1;
+    root[1] = node2;
+    node1.children[0] = unknown % 2 == 0 ? node1 : node2;
+    node1.children[1] = unknown % 3 == 0 ? node1 : node2;
+    node2.children[0] = unknown % 5 == 0 ? node1 : node2;
+    node2.children[1] = unknown % 7 == 0 ? node1 : node2;
+    int idx1 = 0, idx2 = 1, idx3 = 1, idx4 = 0;
+    root[idx1].children[idx2].children[idx3].children[idx4].data = 1;
+    assert (node1.data == 1);
+  }
+}
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc b/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc
new file mode 100644
index 00000000000..92df9c81c8a
--- /dev/null
+++ b/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc
@@ -0,0 +1,14 @@
+CORE
+Test.class
+--function Test.main --show-vcc
+symex_dynamic::dynamic_object6#3\.\.data =
+symex_dynamic::dynamic_object3#3\.\.data =
+^EXIT=0$
+^SIGNAL=0$
+--
+symex_dynamic::dynamic_object6#3\.\.data = symex_dynamic::dynamic_object6#3\.data
+symex_dynamic::dynamic_object3#3\.\.data = symex_dynamic::dynamic_object3#3\.data
+--
+This checks that a write using a mix of field and array accessors uses a field-sensitive
+symbol (the data field of the possible ultimate target objects) rather than using
+a whole-struct write followed by an expansion.
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index ebd9ffc2988..2be68f579eb 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -135,6 +135,25 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   parse_java_language_options(cmdline, options);
   parse_java_object_factory_options(cmdline, options);
 
+  if(cmdline.isset("max-field-sensitivity-array-size"))
+  {
+    options.set_option(
+      "max-field-sensitivity-array-size",
+      cmdline.get_value("max-field-sensitivity-array-size"));
+  }
+
+  if(cmdline.isset("no-array-field-sensitivity"))
+  {
+    if(cmdline.isset("max-field-sensitivity-array-size"))
+    {
+      log.error()
+        << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
+        << " must not be given together" << messaget::eom;
+      exit(CPROVER_EXIT_USAGE_ERROR);
+    }
+    options.set_option("no-array-field-sensitivity", true);
+  }
+
   if(cmdline.isset("show-symex-strategies"))
   {
     log.status() << show_path_strategies() << messaget::eom;
diff --git a/regression/cbmc-concurrency/norace_array1/test.desc b/regression/cbmc-concurrency/norace_array1/test.desc
index c239dca4b31..8ecf05b6d5c 100644
--- a/regression/cbmc-concurrency/norace_array1/test.desc
+++ b/regression/cbmc-concurrency/norace_array1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG pthread
+CORE pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/norace_array2/test.desc b/regression/cbmc-concurrency/norace_array2/test.desc
index c239dca4b31..8ecf05b6d5c 100644
--- a/regression/cbmc-concurrency/norace_array2/test.desc
+++ b/regression/cbmc-concurrency/norace_array2/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG pthread
+CORE pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-concurrency/struct_and_array1/test.desc b/regression/cbmc-concurrency/struct_and_array1/test.desc
index 52168c7eba4..8ecf05b6d5c 100644
--- a/regression/cbmc-concurrency/struct_and_array1/test.desc
+++ b/regression/cbmc-concurrency/struct_and_array1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE pthread
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Multi_Dimensional_Array3/test.desc b/regression/cbmc/Multi_Dimensional_Array3/test.desc
index 9efefbc7362..ba46c0308cf 100644
--- a/regression/cbmc/Multi_Dimensional_Array3/test.desc
+++ b/regression/cbmc/Multi_Dimensional_Array3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
@@ -6,3 +6,6 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+With the SMT backend this incorrect result because of the bug documented here:
+https://github.com/diffblue/cbmc/issues/4749
diff --git a/regression/cbmc/address_space_size_limit3/main.i b/regression/cbmc/address_space_size_limit3/main.i
index ab817d9e0bb..7d4d08cd2ed 100644
--- a/regression/cbmc/address_space_size_limit3/main.i
+++ b/regression/cbmc/address_space_size_limit3/main.i
@@ -92,6 +92,11 @@ void f__L_0x3c6_0()
 
 int main()
 {
+  int unknown;
+  // Avoid constant propagation solving for pointer-offsets of esp,
+  // which prevent demonstrating the object-size limitation this test
+  // intends to exhibit:
+  esp -= (unknown & 1);
   L_0x3fe_0: esp-=0x4;
   L_0x3fe_1: *(uint32_t*)(esp)=ebp;
   L_0x3ff_0: ebp=esp;
diff --git a/regression/cbmc/array-cell-sensitivity1/test.c b/regression/cbmc/array-cell-sensitivity1/test.c
new file mode 100644
index 00000000000..5f10a1405d8
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity1/test.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  int array[10];
+  array[argc] = 1;
+  array[1] = argc;
+  assert(array[1] == argc);
+}
diff --git a/regression/cbmc/array-cell-sensitivity1/test.desc b/regression/cbmc/array-cell-sensitivity1/test.desc
new file mode 100644
index 00000000000..89d5291e18f
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity1/test.desc
@@ -0,0 +1,21 @@
+CORE
+test.c
+--show-vcc
+main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
+main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
+main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
+main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
+main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
+main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
+main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
+main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
+main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
+main::1::array!0@1#3\[\[1\]\] =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::array!0@1#[2-9]\[[0-9]+\]
+--
+This checks that a write with a non-constant index leads to a whole-array
+operation followed by expansion into individual array cells, while a write with
+a constant index leads to direct use of a single cell symbol
diff --git a/regression/cbmc/array-cell-sensitivity1/test_execution.desc b/regression/cbmc/array-cell-sensitivity1/test_execution.desc
new file mode 100644
index 00000000000..9280dcb19be
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity1/test_execution.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.
diff --git a/regression/cbmc/array-cell-sensitivity10/test.c b/regression/cbmc/array-cell-sensitivity10/test.c
new file mode 100644
index 00000000000..3c00351e5bf
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity10/test.c
@@ -0,0 +1,18 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A array[10];
+  struct A other[2];
+  struct A *ptr = argc % 2 ? &other : &array[0];
+  ptr[argc].x = 1;
+  ptr[1].x = argc;
+  assert(ptr[1].x == argc);
+  assert(array[1].x == argc);
+}
diff --git a/regression/cbmc/array-cell-sensitivity10/test.desc b/regression/cbmc/array-cell-sensitivity10/test.desc
new file mode 100644
index 00000000000..1061132428e
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity10/test.desc
@@ -0,0 +1,32 @@
+CORE
+test.c
+--show-vcc
+main::1::array!0@1#2\[\[0\]\]..x = main::1::array!0@1#1\[0\].x
+main::1::array!0@1#2\[\[1\]\]..x = main::1::array!0@1#1\[1\].x
+main::1::array!0@1#2\[\[2\]\]..x = main::1::array!0@1#1\[2\].x
+main::1::array!0@1#2\[\[3\]\]..x = main::1::array!0@1#1\[3\].x
+main::1::array!0@1#2\[\[4\]\]..x = main::1::array!0@1#1\[4\].x
+main::1::array!0@1#2\[\[5\]\]..x = main::1::array!0@1#1\[5\].x
+main::1::array!0@1#2\[\[6\]\]..x = main::1::array!0@1#1\[6\].x
+main::1::array!0@1#2\[\[7\]\]..x = main::1::array!0@1#1\[7\].x
+main::1::array!0@1#2\[\[8\]\]..x = main::1::array!0@1#1\[8\].x
+main::1::array!0@1#2\[\[9\]\]..x = main::1::array!0@1#1\[9\].x
+main::1::array!0@1#3\[\[1\]\]..x =
+main::1::array!0@1#2\[\[0\]\]..y = main::1::array!0@1#1\[0\].y
+main::1::array!0@1#2\[\[1\]\]..y = main::1::array!0@1#1\[1\].y
+main::1::array!0@1#2\[\[2\]\]..y = main::1::array!0@1#1\[2\].y
+main::1::array!0@1#2\[\[3\]\]..y = main::1::array!0@1#1\[3\].y
+main::1::array!0@1#2\[\[4\]\]..y = main::1::array!0@1#1\[4\].y
+main::1::array!0@1#2\[\[5\]\]..y = main::1::array!0@1#1\[5\].y
+main::1::array!0@1#2\[\[6\]\]..y = main::1::array!0@1#1\[6\].y
+main::1::array!0@1#2\[\[7\]\]..y = main::1::array!0@1#1\[7\].y
+main::1::array!0@1#2\[\[8\]\]..y = main::1::array!0@1#1\[8\].y
+main::1::array!0@1#2\[\[9\]\]..y = main::1::array!0@1#1\[9\].y
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This checks that a write with a non-constant index leads to a whole-array
+operation followed by expansion into individual array cells, while a write with
+a constant index leads to direct use of a single cell symbol, for the case where
+the array element is struct-typed and accessed via a pointer.
diff --git a/regression/cbmc/array-cell-sensitivity10/test_execution.desc b/regression/cbmc/array-cell-sensitivity10/test_execution.desc
new file mode 100644
index 00000000000..1e8aa561e48
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity10/test_execution.desc
@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 16.*SUCCESS$
+^\[main.assertion\.2\] line 17.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.
diff --git a/regression/cbmc/array-cell-sensitivity11/test.c b/regression/cbmc/array-cell-sensitivity11/test.c
new file mode 100644
index 00000000000..2db85d1c016
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity11/test.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A array[10];
+  int *ptr = argc % 2 ? &argc : &array[0].y;
+  *ptr = argc;
+  assert(*ptr == argc);
+  assert(array[1].y == argc);
+}
diff --git a/regression/cbmc/array-cell-sensitivity11/test.desc b/regression/cbmc/array-cell-sensitivity11/test.desc
new file mode 100644
index 00000000000..876777e3cf6
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity11/test.desc
@@ -0,0 +1,12 @@
+CORE
+test.c
+--show-vcc
+main::1::array!0@1#2\[\[0\]\]..y =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::array!0@1#[2-9]\[\[[1-9]\]\]
+main::1::array!0@1#[3-9]\[\[[0-9]\]\]
+--
+This checks that an array access made via a pointer to a member of the array's
+element struct type is executed using a field-sensitive symbol.
diff --git a/regression/cbmc/array-cell-sensitivity11/test_execution.desc b/regression/cbmc/array-cell-sensitivity11/test_execution.desc
new file mode 100644
index 00000000000..d33e4045438
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity11/test_execution.desc
@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 14.*SUCCESS$
+^\[main.assertion\.2\] line 15.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.
diff --git a/regression/cbmc/array-cell-sensitivity12/test.c b/regression/cbmc/array-cell-sensitivity12/test.c
new file mode 100644
index 00000000000..91000e7e791
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity12/test.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A array[10];
+  int *ptr = argc % 2 ? &array[0].x : &array[0].y;
+  *ptr = argc;
+  assert(*ptr == argc);
+  assert(array[0].y == argc);
+}
diff --git a/regression/cbmc/array-cell-sensitivity12/test.desc b/regression/cbmc/array-cell-sensitivity12/test.desc
new file mode 100644
index 00000000000..2392541df5a
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity12/test.desc
@@ -0,0 +1,15 @@
+FUTURE
+test.c
+--show-vcc
+main::1::array!0@1#2\[\[0\]\]..x =
+main::1::array!0@1#2\[\[0\]\]..y =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::array!0@1#[2-9]\[\[[1-9]\]\]
+main::1::array!0@1#[3-9]\[\[[0-9]\]\]
+--
+Ideally we should handle accesses to a pointer with a finite set of possible
+referents precisely, but because value_sett regards &array[0].x and &array[0].y
+as two different offsets into the same allocation and discards the precise offsets
+they point to, this is currently handled imprecisely with a byte_update operation.
diff --git a/regression/cbmc/array-cell-sensitivity12/test_execution.desc b/regression/cbmc/array-cell-sensitivity12/test_execution.desc
new file mode 100644
index 00000000000..d33e4045438
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity12/test_execution.desc
@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 14.*SUCCESS$
+^\[main.assertion\.2\] line 15.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.
diff --git a/regression/cbmc/array-cell-sensitivity13/test.c b/regression/cbmc/array-cell-sensitivity13/test.c
new file mode 100644
index 00000000000..bb1e71dcdc0
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity13/test.c
@@ -0,0 +1,22 @@
+#include <assert.h>
+
+struct A
+{
+  int data;
+  struct A *children[2];
+};
+
+int main(int argc, char **argv)
+{
+  struct A root;
+  struct A node1, node2;
+  root.children[0] = argc % 2 ? &node1 : &node2;
+  root.children[1] = argc % 3 ? &node1 : &node2;
+  node1.children[0] = argc % 5 ? &node1 : &node2;
+  node1.children[1] = argc % 7 ? &node1 : &node2;
+  node2.children[0] = argc % 11 ? &node1 : &node2;
+  node2.children[1] = argc % 13 ? &node1 : &node2;
+  root.children[0]->children[1]->children[1]->children[0]->data = 1;
+  assert(root.children[0]->children[1]->children[1]->children[0]->data == 1);
+  assert(node1.data == argc);
+}
diff --git a/regression/cbmc/array-cell-sensitivity13/test.desc b/regression/cbmc/array-cell-sensitivity13/test.desc
new file mode 100644
index 00000000000..36d5cc34e1a
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity13/test.desc
@@ -0,0 +1,13 @@
+CORE
+test.c
+--show-vcc
+main::1::node1!0@1#2\.\.data =
+main::1::node2!0@1#2\.\.data =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::node1!0@1#[3-9]\.\.children\[\[[01]\]\] =
+--
+This checks that mixed array and field accesses are executed using a field-sensitive
+symbol (main::1::node1!0@1#2..data) rather than by assigning the whole struct and
+expanding into field symbols (which would assign main::1::node1!0@1#3..children\[\[[01]\]\])
diff --git a/regression/cbmc/array-cell-sensitivity13/test_execution.desc b/regression/cbmc/array-cell-sensitivity13/test_execution.desc
new file mode 100644
index 00000000000..f3dc42bc691
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity13/test_execution.desc
@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 20.*SUCCESS$
+^\[main.assertion\.2\] line 21.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.
diff --git a/regression/cbmc/array-cell-sensitivity14/test.c b/regression/cbmc/array-cell-sensitivity14/test.c
new file mode 100644
index 00000000000..ddec5e9b295
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity14/test.c
@@ -0,0 +1,25 @@
+#include <assert.h>
+
+struct A
+{
+  int data;
+  struct A *children[2];
+};
+
+int main(int argc, char **argv)
+{
+  struct A root;
+  struct A node1, node2;
+  root.children[0] = argc % 2 ? &node1 : &node2;
+  root.children[1] = argc % 3 ? &node1 : &node2;
+  node1.children[0] = argc % 5 ? &node1 : &node2;
+  node1.children[1] = argc % 7 ? &node1 : &node2;
+  node2.children[0] = argc % 11 ? &node1 : &node2;
+  node2.children[1] = argc % 13 ? &node1 : &node2;
+  int idx1 = 0, idx2 = 1, idx3 = 1, idx4 = 0;
+  root.children[idx1]->children[idx2]->children[idx3]->children[idx4]->data = 1;
+  assert(
+    root.children[idx1]->children[idx2]->children[idx3]->children[idx4]->data ==
+    1);
+  assert(node1.data == argc);
+}
diff --git a/regression/cbmc/array-cell-sensitivity14/test.desc b/regression/cbmc/array-cell-sensitivity14/test.desc
new file mode 100644
index 00000000000..3395875c67d
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity14/test.desc
@@ -0,0 +1,14 @@
+CORE
+test.c
+--show-vcc
+main::1::node1!0@1#2\.\.data =
+main::1::node2!0@1#2\.\.data =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::node1!0@1#[3-9]\.\.children\[\[[01]\]\] =
+--
+This checks that mixed array and field accesses are executed using a field-sensitive
+symbol (main::1::node1!0@1#2..data) rather than by assigning the whole struct and
+expanding into field symbols (which would assign main::1::node1!0@1#3..children\[\[[01]\]\]),
+for the case where the array indices only become constant after propagation.
diff --git a/regression/cbmc/array-cell-sensitivity14/test_execution.desc b/regression/cbmc/array-cell-sensitivity14/test_execution.desc
new file mode 100644
index 00000000000..5b84583d54a
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity14/test_execution.desc
@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 21.*SUCCESS$
+^\[main.assertion\.2\] line 24.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.
diff --git a/regression/cbmc/array-cell-sensitivity2/test.c b/regression/cbmc/array-cell-sensitivity2/test.c
new file mode 100644
index 00000000000..729ef6bd682
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity2/test.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  int array[argc];
+  array[argc - 1] = 1;
+  array[1] = argc;
+  assert(array[1] == argc);
+}
diff --git a/regression/cbmc/array-cell-sensitivity2/test.desc b/regression/cbmc/array-cell-sensitivity2/test.desc
new file mode 100644
index 00000000000..92a0b40af63
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity2/test.desc
@@ -0,0 +1,13 @@
+CORE
+test.c
+--show-vcc
+main::1::array!0@1#2 = with\(main::1::array!0@1#1, cast\(-1 \+ main::argc!0@1#1, signedbv\[64\]\), 1\)
+main::1::array!0@1#3 = with\(main::1::array!0@1#2, 1, main::argc!0@1#1\)
+^EXIT=0$
+^SIGNAL=0$
+--
+\[\[[0-9]+\]\]
+--
+This checks that arrays of uncertain size are always treated as aggregates and
+are not expanded into individual cell symbols (which use the [[index]] notation
+to distinguish them from the index operator (array[index]))
diff --git a/regression/cbmc/array-cell-sensitivity2/test_execution.desc b/regression/cbmc/array-cell-sensitivity2/test_execution.desc
new file mode 100644
index 00000000000..9280dcb19be
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity2/test_execution.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.
diff --git a/regression/cbmc/array-cell-sensitivity3/test.c b/regression/cbmc/array-cell-sensitivity3/test.c
new file mode 100644
index 00000000000..cc33ade48c7
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity3/test.c
@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  int array[10];
+  int *ptr = argc % 2 ? &argc : &array[0];
+  ptr[argc] = 1;
+  ptr[1] = argc;
+  assert(ptr[1] == argc);
+  assert(array[1] == argc);
+}
diff --git a/regression/cbmc/array-cell-sensitivity3/test.desc b/regression/cbmc/array-cell-sensitivity3/test.desc
new file mode 100644
index 00000000000..da0a7025fda
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity3/test.desc
@@ -0,0 +1,23 @@
+CORE
+test.c
+--show-vcc
+main::1::array!0@1#2\[\[0]\] = main::1::array!0@1#1\[0\]
+main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
+main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
+main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
+main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
+main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
+main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
+main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
+main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
+main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
+main::1::array!0@1#3\[\[1\]\] =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::array!0@1#[2-9]\[[0-9]+\]
+--
+This checks that a write with a non-constant index leads to a whole-array
+operation followed by expansion into individual array cells, while a write with
+a constant index leads to direct use of a single cell symbol, even when the
+array is accessed via a pointer with other possible aliases.
diff --git a/regression/cbmc/array-cell-sensitivity3/test_execution.desc b/regression/cbmc/array-cell-sensitivity3/test_execution.desc
new file mode 100644
index 00000000000..52bf413ffd9
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity3/test_execution.desc
@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 9.*SUCCESS$
+^\[main.assertion\.2\] line 10.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.
diff --git a/regression/cbmc/array-cell-sensitivity4/test.c b/regression/cbmc/array-cell-sensitivity4/test.c
new file mode 100644
index 00000000000..99dae61d3e9
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity4/test.c
@@ -0,0 +1,10 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  int array[10];
+  int x = 1;
+  array[argc] = 1;
+  array[x] = argc;
+  assert(array[1] == argc);
+}
diff --git a/regression/cbmc/array-cell-sensitivity4/test.desc b/regression/cbmc/array-cell-sensitivity4/test.desc
new file mode 100644
index 00000000000..9f7da1d30cc
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity4/test.desc
@@ -0,0 +1,21 @@
+CORE
+test.c
+--show-vcc
+main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
+main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
+main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
+main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
+main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
+main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
+main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
+main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
+main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
+main::1::array!0@1#3\[\[1\]\] =
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This checks that a write with a non-constant index leads to a whole-array
+operation followed by expansion into individual array cells, while a write with
+a constant index leads to direct use of a single cell symbol, even when the
+constant index is only revealed as constant after propagation.
diff --git a/regression/cbmc/array-cell-sensitivity4/test_execution.desc b/regression/cbmc/array-cell-sensitivity4/test_execution.desc
new file mode 100644
index 00000000000..9280dcb19be
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity4/test_execution.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.
diff --git a/regression/cbmc/array-cell-sensitivity5/test.c b/regression/cbmc/array-cell-sensitivity5/test.c
new file mode 100644
index 00000000000..1d0d3b14ece
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity5/test.c
@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main(int argc, char **argv)
+{
+  int *array = malloc(sizeof(int) * 10);
+  array[argc] = 1;
+  array[1] = argc;
+  assert(array[1] == argc);
+}
diff --git a/regression/cbmc/array-cell-sensitivity5/test.desc b/regression/cbmc/array-cell-sensitivity5/test.desc
new file mode 100644
index 00000000000..923d28fc391
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity5/test.desc
@@ -0,0 +1,22 @@
+CORE
+test.c
+--show-vcc
+symex_dynamic::dynamic_object1#2\[\[1\]\] = symex_dynamic::dynamic_object1#2\[1\]
+symex_dynamic::dynamic_object1#2\[\[2\]\] = symex_dynamic::dynamic_object1#2\[2\]
+symex_dynamic::dynamic_object1#2\[\[3\]\] = symex_dynamic::dynamic_object1#2\[3\]
+symex_dynamic::dynamic_object1#2\[\[4\]\] = symex_dynamic::dynamic_object1#2\[4\]
+symex_dynamic::dynamic_object1#2\[\[5\]\] = symex_dynamic::dynamic_object1#2\[5\]
+symex_dynamic::dynamic_object1#2\[\[6\]\] = symex_dynamic::dynamic_object1#2\[6\]
+symex_dynamic::dynamic_object1#2\[\[7\]\] = symex_dynamic::dynamic_object1#2\[7\]
+symex_dynamic::dynamic_object1#2\[\[8\]\] = symex_dynamic::dynamic_object1#2\[8\]
+symex_dynamic::dynamic_object1#2\[\[9\]\] = symex_dynamic::dynamic_object1#2\[9\]
+symex_dynamic::dynamic_object1#3\[\[1\]\] =
+^EXIT=0$
+^SIGNAL=0$
+--
+symex_dynamic::dynamic_object1#[3-9]\[[0-9]+\]
+--
+This checks that a write with a non-constant index leads to a whole-array
+operation followed by expansion into individual array cells, while a write with
+a constant index leads to direct use of a single cell symbol, even when the array
+in question is dynamically allocated.
diff --git a/regression/cbmc/array-cell-sensitivity5/test_execution.desc b/regression/cbmc/array-cell-sensitivity5/test_execution.desc
new file mode 100644
index 00000000000..9280dcb19be
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity5/test_execution.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.
diff --git a/regression/cbmc/array-cell-sensitivity6/test.c b/regression/cbmc/array-cell-sensitivity6/test.c
new file mode 100644
index 00000000000..fc36a10f6f2
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity6/test.c
@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main(int argc, char **argv)
+{
+  int x = 10;
+  int *array = malloc(sizeof(int) * x);
+  array[argc] = 1;
+  array[1] = argc;
+  assert(array[1] == argc);
+}
diff --git a/regression/cbmc/array-cell-sensitivity6/test.desc b/regression/cbmc/array-cell-sensitivity6/test.desc
new file mode 100644
index 00000000000..cdbfa2c3aac
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity6/test.desc
@@ -0,0 +1,23 @@
+CORE
+test.c
+--show-vcc
+symex_dynamic::dynamic_object1#2\[\[1\]\] = symex_dynamic::dynamic_object1#2\[1\]
+symex_dynamic::dynamic_object1#2\[\[2\]\] = symex_dynamic::dynamic_object1#2\[2\]
+symex_dynamic::dynamic_object1#2\[\[3\]\] = symex_dynamic::dynamic_object1#2\[3\]
+symex_dynamic::dynamic_object1#2\[\[4\]\] = symex_dynamic::dynamic_object1#2\[4\]
+symex_dynamic::dynamic_object1#2\[\[5\]\] = symex_dynamic::dynamic_object1#2\[5\]
+symex_dynamic::dynamic_object1#2\[\[6\]\] = symex_dynamic::dynamic_object1#2\[6\]
+symex_dynamic::dynamic_object1#2\[\[7\]\] = symex_dynamic::dynamic_object1#2\[7\]
+symex_dynamic::dynamic_object1#2\[\[8\]\] = symex_dynamic::dynamic_object1#2\[8\]
+symex_dynamic::dynamic_object1#2\[\[9\]\] = symex_dynamic::dynamic_object1#2\[9\]
+symex_dynamic::dynamic_object1#3\[\[1\]\] =
+^EXIT=0$
+^SIGNAL=0$
+--
+symex_dynamic::dynamic_object1#[3-9]\[[0-9]+\]
+--
+This checks that a write with a non-constant index leads to a whole-array
+operation followed by expansion into individual array cells, while a write with
+a constant index leads to direct use of a single cell symbol, even when the array
+in question is dynamically allocated and the constancy of its size depends on
+constant propagation.
diff --git a/regression/cbmc/array-cell-sensitivity6/test_execution.desc b/regression/cbmc/array-cell-sensitivity6/test_execution.desc
new file mode 100644
index 00000000000..9280dcb19be
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity6/test_execution.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.
diff --git a/regression/cbmc/array-cell-sensitivity7/test.c b/regression/cbmc/array-cell-sensitivity7/test.c
new file mode 100644
index 00000000000..48f8f85a7e6
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity7/test.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main(int argc, char **argv)
+{
+  int array[10];
+  char *ptr = argc % 2 ? (char *)&array[0] : (char *)&argc;
+  ptr[argc] = 'a';
+  ptr[1] = (char)argc;
+  assert(ptr[1] == (char)argc);
+  assert(array[1] == (char)argc);
+}
diff --git a/regression/cbmc/array-cell-sensitivity7/test.desc b/regression/cbmc/array-cell-sensitivity7/test.desc
new file mode 100644
index 00000000000..ffd25206574
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity7/test.desc
@@ -0,0 +1,23 @@
+CORE
+test.c
+--show-vcc
+main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
+main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
+main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
+main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
+main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
+main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
+main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
+main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
+main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
+main::1::array!0@1#3\[\[0\]\] =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::array!0@1#[2-9]\[[0-9]+\]
+main::1::array!0@1#3\[\[[1-9]\]\] =
+--
+This checks that a write with a non-constant index leads to a whole-array
+operation followed by expansion into individual array cells, while a write with
+a constant index leads to direct use of a single cell symbol, even when the array
+is addressed via a pointer cast to a smaller type.
diff --git a/regression/cbmc/array-cell-sensitivity7/test_execution.desc b/regression/cbmc/array-cell-sensitivity7/test_execution.desc
new file mode 100644
index 00000000000..62502389e48
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity7/test_execution.desc
@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 10.*SUCCESS$
+^\[main.assertion\.2\] line 11.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.
diff --git a/regression/cbmc/array-cell-sensitivity8/test.c b/regression/cbmc/array-cell-sensitivity8/test.c
new file mode 100644
index 00000000000..8874633f1fa
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity8/test.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main(int argc, char **argv)
+{
+  int array[10];
+  long long other;
+  long long *ptr = argc % 2 ? (long long *)&array[0] : &other;
+  ptr[argc] = 1;
+  ptr[1] = argc;
+  assert(ptr[1] == argc);
+  assert(array[1] == argc);
+}
diff --git a/regression/cbmc/array-cell-sensitivity8/test.desc b/regression/cbmc/array-cell-sensitivity8/test.desc
new file mode 100644
index 00000000000..da8e78103f9
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity8/test.desc
@@ -0,0 +1,30 @@
+CORE
+test.c
+--show-vcc
+main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
+main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
+main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
+main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
+main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
+main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
+main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
+main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
+main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
+main::1::array!0@1#2 =.*byte_extract_little_endian
+main::1::array!0@1#3\[\[0\]\] = main::1::array!0@1#2\[0\]
+main::1::array!0@1#3\[\[1\]\] = main::1::array!0@1#2\[1\]
+main::1::array!0@1#3\[\[2\]\] = main::1::array!0@1#2\[2\]
+main::1::array!0@1#3\[\[3\]\] = main::1::array!0@1#2\[3\]
+main::1::array!0@1#3\[\[4\]\] = main::1::array!0@1#2\[4\]
+main::1::array!0@1#3\[\[5\]\] = main::1::array!0@1#2\[5\]
+main::1::array!0@1#3\[\[6\]\] = main::1::array!0@1#2\[6\]
+main::1::array!0@1#3\[\[7\]\] = main::1::array!0@1#2\[7\]
+main::1::array!0@1#3\[\[8\]\] = main::1::array!0@1#2\[8\]
+main::1::array!0@1#3\[\[9\]\] = main::1::array!0@1#2\[9\]
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This checks that when an array cell is accessed via a pointer to a large enough
+type that multiple cells are required then whole-array operations are used,
+rather than attempting to operate on single cell symbols.
diff --git a/regression/cbmc/array-cell-sensitivity8/test_execution.desc b/regression/cbmc/array-cell-sensitivity8/test_execution.desc
new file mode 100644
index 00000000000..96db1c25647
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity8/test_execution.desc
@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 11.*SUCCESS$
+^\[main.assertion\.2\] line 12.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.
diff --git a/regression/cbmc/array-cell-sensitivity9/test.c b/regression/cbmc/array-cell-sensitivity9/test.c
new file mode 100644
index 00000000000..d675d409c81
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity9/test.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A array[10];
+  array[argc].x = 1;
+  array[1].x = argc;
+  assert(array[1].x == argc);
+}
diff --git a/regression/cbmc/array-cell-sensitivity9/test.desc b/regression/cbmc/array-cell-sensitivity9/test.desc
new file mode 100644
index 00000000000..1a7d5937ac2
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity9/test.desc
@@ -0,0 +1,32 @@
+CORE
+test.c
+--show-vcc
+main::1::array!0@1#2\[\[0\]\]..x = main::1::array!0@1#1\[0\].x
+main::1::array!0@1#2\[\[1\]\]..x = main::1::array!0@1#1\[1\].x
+main::1::array!0@1#2\[\[2\]\]..x = main::1::array!0@1#1\[2\].x
+main::1::array!0@1#2\[\[3\]\]..x = main::1::array!0@1#1\[3\].x
+main::1::array!0@1#2\[\[4\]\]..x = main::1::array!0@1#1\[4\].x
+main::1::array!0@1#2\[\[5\]\]..x = main::1::array!0@1#1\[5\].x
+main::1::array!0@1#2\[\[6\]\]..x = main::1::array!0@1#1\[6\].x
+main::1::array!0@1#2\[\[7\]\]..x = main::1::array!0@1#1\[7\].x
+main::1::array!0@1#2\[\[8\]\]..x = main::1::array!0@1#1\[8\].x
+main::1::array!0@1#2\[\[9\]\]..x = main::1::array!0@1#1\[9\].x
+main::1::array!0@1#3\[\[1\]\]..x =
+main::1::array!0@1#2\[\[0\]\]..y = main::1::array!0@1#1\[0\].y
+main::1::array!0@1#2\[\[1\]\]..y = main::1::array!0@1#1\[1\].y
+main::1::array!0@1#2\[\[2\]\]..y = main::1::array!0@1#1\[2\].y
+main::1::array!0@1#2\[\[3\]\]..y = main::1::array!0@1#1\[3\].y
+main::1::array!0@1#2\[\[4\]\]..y = main::1::array!0@1#1\[4\].y
+main::1::array!0@1#2\[\[5\]\]..y = main::1::array!0@1#1\[5\].y
+main::1::array!0@1#2\[\[6\]\]..y = main::1::array!0@1#1\[6\].y
+main::1::array!0@1#2\[\[7\]\]..y = main::1::array!0@1#1\[7\].y
+main::1::array!0@1#2\[\[8\]\]..y = main::1::array!0@1#1\[8\].y
+main::1::array!0@1#2\[\[9\]\]..y = main::1::array!0@1#1\[9\].y
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This checks that a write with a non-constant index leads to a whole-array
+operation followed by expansion into individual array cells, while a write with
+a constant index leads to direct use of a single cell symbol, for the case where
+the array element is struct-typed.
diff --git a/regression/cbmc/array-cell-sensitivity9/test_execution.desc b/regression/cbmc/array-cell-sensitivity9/test_execution.desc
new file mode 100644
index 00000000000..9280dcb19be
--- /dev/null
+++ b/regression/cbmc/array-cell-sensitivity9/test_execution.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.
diff --git a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc
index 22f1388d331..df655168340 100644
--- a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc
+++ b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc
@@ -1,7 +1,7 @@
 CORE
 double_deref_with_pointer_arithmetic.c
 --show-vcc
-^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = symex_dynamic::dynamic_object1#3\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
+^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
 ^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\)
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc/trace-values/trace-values.desc b/regression/cbmc/trace-values/trace-values.desc
index b64fd79b8bf..c9a7e9a3cac 100644
--- a/regression/cbmc/trace-values/trace-values.desc
+++ b/regression/cbmc/trace-values/trace-values.desc
@@ -9,10 +9,14 @@ trace-values.c
 ^  local_var=3 .*$
 ^  my_nested\[0.*\].array\[1.*\]=4 .*$
 ^  my_nested\[1.*\].f=5 .*$
-^  null\$object=6 .*$
 ^  junk\$object=7 .*$
 ^  dynamic_object1\[1.*\]=8 .*$
-^  my_nested\[1.*\]=\{ .f=0, .array=\{ 0, 4, 0 \} \} .*$
+^  my_nested\[1.*\](=\{ )?.f=0[ ,]
+^  my_nested\[1.*\](=\{ .f=0, )?.array=\{ 0, 4, 0 \}
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
+--
+Note the assignment to "null" is not included because an assignment direct to
+a certainly-null pointer goes to symex::invalid_object, not null$object, and is
+hidden from the --trace output.
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 2c74dd4a826..48e3df60fe1 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -147,6 +147,25 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
+  if(cmdline.isset("max-field-sensitivity-array-size"))
+  {
+    options.set_option(
+      "max-field-sensitivity-array-size",
+      cmdline.get_value("max-field-sensitivity-array-size"));
+  }
+
+  if(cmdline.isset("no-array-field-sensitivity"))
+  {
+    if(cmdline.isset("max-field-sensitivity-array-size"))
+    {
+      log.error()
+        << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
+        << " must not be given together" << messaget::eom;
+      exit(CPROVER_EXIT_USAGE_ERROR);
+    }
+    options.set_option("no-array-field-sensitivity", true);
+  }
+
   if(cmdline.isset("partial-loops") && cmdline.isset("unwinding-assertions"))
   {
     log.error()
diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h
index 3eaf779efdd..99c17dd0f47 100644
--- a/src/goto-checker/bmc_util.h
+++ b/src/goto-checker/bmc_util.h
@@ -186,7 +186,8 @@ void run_property_decider(
   "(show-symex-strategies)" \
   "(depth):" \
   "(unwind):" \
-  "(unwindset):" \
+  "(max-field-sensitivity-array-size):" \
+  "(no-array-field-sensitivity)" \
   "(graphml-witness):" \
   "(unwindset):"
 
@@ -198,6 +199,15 @@ void run_property_decider(
   " --program-only               only show program expression\n" \
   " --show-loops                 show the loops in the program\n" \
   " --depth nr                   limit search depth\n" \
+  " --max-field-sensitivity-array-size M\n" \
+  "                              maximum size M of arrays for which field\n" \
+  "                              sensitivity will be applied to array,\n" \
+  "                              the default is 64\n" \
+  " --no-array-field-sensitivity\n" \
+  "                              deactivate field sensitivity for arrays, " \
+  "this is\n" \
+  "                              equivalent to setting the maximum field \n" \
+  "                              sensitivity size for arrays to 0\n" \
   " --unwind nr                  unwind nr times\n" \
   " --unwindset L:B,...          unwind loop L with a bound of B\n" \
   "                              (use --show-loops to get the loop IDs)\n" \
diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp
index 608dd300605..63b9b4cc863 100644
--- a/src/goto-instrument/accelerate/scratch_program.cpp
+++ b/src/goto-instrument/accelerate/scratch_program.cpp
@@ -38,6 +38,7 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
 
   symex_state = util_make_unique<goto_symex_statet>(
     symex_targett::sourcet(goto_functionst::entry_point(), *this),
+    symex.field_sensitivity,
     guard_manager,
     [this](const irep_idt &id) {
       return path_storage.get_unique_l2_index(id);
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 60be0403b6e..5b1a243a5da 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -370,11 +370,13 @@ void build_goto_trace(
 
       if(SSA_step.original_full_lhs.is_not_nil())
       {
-        goto_trace_step.full_lhs = build_full_lhs_rec(
-          decision_procedure,
-          ns,
-          SSA_step.original_full_lhs,
-          SSA_step.ssa_full_lhs);
+        goto_trace_step.full_lhs = simplify_expr(
+          build_full_lhs_rec(
+            decision_procedure,
+            ns,
+            SSA_step.original_full_lhs,
+            SSA_step.ssa_full_lhs),
+          ns);
         replace_nondet_in_type(goto_trace_step.full_lhs, decision_procedure);
       }
 
diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp
index fc05ad82213..0e5cbd09c14 100644
--- a/src/goto-symex/field_sensitivity.cpp
+++ b/src/goto-symex/field_sensitivity.cpp
@@ -16,7 +16,7 @@ Author: Michael Tautschnig
 #include "goto_symex_state.h"
 #include "symex_target.h"
 
-// #define ENABLE_ARRAY_FIELD_SENSITIVITY
+#define ENABLE_ARRAY_FIELD_SENSITIVITY
 
 exprt field_sensitivityt::apply(
   const namespacet &ns,
@@ -96,15 +96,48 @@ exprt field_sensitivityt::apply(
       // place the entire index expression, not just the array operand, in an
       // SSA expression
       ssa_exprt tmp = to_ssa_expr(index.array());
+      auto l2_index = state.rename(index.index(), ns);
+      l2_index.simplify(ns);
       bool was_l2 = !tmp.get_level_2().empty();
+      exprt l2_size =
+        state.rename(to_array_type(index.array().type()).size(), ns).get();
+      if(l2_size.is_nil() && index.array().id() == ID_symbol)
+      {
+        // In case the array type was incomplete, attempt to retrieve it from
+        // the symbol table.
+        const symbolt *array_from_symbol_table = ns.get_symbol_table().lookup(
+          to_symbol_expr(index.array()).get_identifier());
+        if(array_from_symbol_table != nullptr)
+          l2_size = to_array_type(array_from_symbol_table->type).size();
+      }
 
-      tmp.remove_level_2();
-      index.array() = tmp.get_original_expr();
-      tmp.set_expression(index);
-      if(was_l2)
-        return state.rename(std::move(tmp), ns).get();
-      else
-        return std::move(tmp);
+      if(
+        l2_size.id() == ID_constant &&
+        numeric_cast_v<mp_integer>(to_constant_expr(l2_size)) <=
+          max_field_sensitivity_array_size)
+      {
+        if(l2_index.get().id() == ID_constant)
+        {
+          // place the entire index expression, not just the array operand,
+          // in an SSA expression
+          ssa_exprt ssa_array = to_ssa_expr(index.array());
+          ssa_array.remove_level_2();
+          index.array() = ssa_array.get_original_expr();
+          index.index() = l2_index.get();
+          tmp.set_expression(index);
+          if(was_l2)
+            return state.rename(std::move(tmp), ns).get();
+          else
+            return std::move(tmp);
+        }
+        else if(!write)
+        {
+          // Expand the array and return `{array[0]; array[1]; ...}[index]`
+          exprt expanded_array =
+            get_fields(ns, state, to_ssa_expr(index.array()));
+          return index_exprt{std::move(expanded_array), index.index()};
+        }
+      }
     }
   }
 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
@@ -147,7 +180,10 @@ 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)
+    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)
   {
     const array_typet &type = to_array_type(ssa_expr.type());
     const std::size_t array_size =
@@ -267,8 +303,10 @@ void field_sensitivityt::field_assignments_rec(
   {
     const std::size_t array_size =
       numeric_cast_v<std::size_t>(to_constant_expr(type->size()));
-    PRECONDITION(
-      lhs_fs.has_operands() && lhs_fs.operands().size() == array_size);
+    PRECONDITION(lhs_fs.operands().size() == array_size);
+
+    if(array_size > max_field_sensitivity_array_size)
+      return;
 
     exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
     for(std::size_t i = 0; i < array_size; ++i)
@@ -301,7 +339,7 @@ void field_sensitivityt::field_assignments_rec(
   }
 }
 
-bool field_sensitivityt::is_divisible(const ssa_exprt &expr)
+bool field_sensitivityt::is_divisible(const ssa_exprt &expr) const
 {
   if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag)
     return true;
@@ -309,7 +347,9 @@ bool field_sensitivityt::is_divisible(const ssa_exprt &expr)
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   if(
     expr.type().id() == ID_array &&
-    to_array_type(expr.type()).size().id() == ID_constant)
+    to_array_type(expr.type()).size().id() == ID_constant &&
+    numeric_cast_v<mp_integer>(to_constant_expr(
+      to_array_type(expr.type()).size())) <= max_field_sensitivity_array_size)
   {
     return true;
   }
diff --git a/src/goto-symex/field_sensitivity.h b/src/goto-symex/field_sensitivity.h
index 8846285b1b5..0b791ce694a 100644
--- a/src/goto-symex/field_sensitivity.h
+++ b/src/goto-symex/field_sensitivity.h
@@ -9,6 +9,8 @@ Author: Michael Tautschnig
 #ifndef CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
 #define CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
 
+#include <util/magic.h>
+
 class exprt;
 class ssa_exprt;
 class namespacet;
@@ -26,9 +28,10 @@ class symex_targett;
 /// Note that field sensitivity is not applied as a single pass over the
 /// whole goto program but instead applied as the symbolic execution unfolds.
 ///
-/// On a high level, field sensitivity replaces member operators with atomic
-/// symbols representing a field when possible. In cases where this is not
-/// immediately possible, like struct assignments, some things need to be added.
+/// On a high level, field sensitivity replaces member operators, and array
+/// accesses with atomic symbols representing a field when possible.
+/// In cases where this is not immediately possible, like struct assignments,
+/// some things need to be added.
 /// The possible cases are described below.
 ///
 /// ### Member access
@@ -50,9 +53,40 @@ class symex_targett;
 /// `struct_expr..field_name1 = other_struct..field_name1;`
 /// `struct_expr..field_name2 = other_struct..field_name2;` etc.
 /// See \ref field_sensitivityt::field_assignments.
+///
+/// ### Array access
+/// An index expression `array[index]` when index is constant and array has
+/// constant size is replaced by the symbol `array[[index]]`; note the use
+/// of `[[` and `]]` to visually distinguish the symbol from the index
+/// expression.
+/// When `index` is not a constant, `array[index]` is replaced by
+///  `{array[[0]]; array[[1]]; …index]`.
+/// Note that this process does not apply to arrays whose size is not constant,
+/// and arrays whose size exceed the bound \c max_field_sensitivity_array_size.
+/// See \ref field_sensitivityt::apply.
+///
+/// ### Symbols representing arrays
+/// In an rvalue, a symbol `array` which has array type will be replaced by
+/// `{array[[0]]; array[[1]]; …}[index]`.
+/// See \ref field_sensitivityt::get_fields.
+///
+/// ### Assignment to an array
+/// When the array symbol is on the left-hand-side, for instance for
+/// an assignment `array = other_array`, the assignment is replaced by a
+/// sequence of assignments:
+/// `array[[0]] = other_array[[0]]`;
+/// `array[[1]] = other_array[[1]]`; etc.
+/// See \ref field_sensitivityt::field_assignments.
 class field_sensitivityt
 {
 public:
+  /// \param max_array_size: maximum size for which field sensitivity will be
+  ///   applied to array cells
+  explicit field_sensitivityt(std::size_t max_array_size)
+    : max_field_sensitivity_array_size(max_array_size)
+  {
+  }
+
   /// Assign to the individual fields of a non-expanded symbol \p lhs. This is
   /// required whenever prior steps have updated the full object rather than
   /// individual fields, e.g., in case of assignments to an array at an unknown
@@ -106,12 +140,14 @@ class field_sensitivityt
   /// \param expr: the expression to evaluate
   /// \return False, if and only if, \p expr would be a single field-sensitive
   /// SSA expression.
-  static bool is_divisible(const ssa_exprt &expr);
+  bool is_divisible(const ssa_exprt &expr) const;
 
 private:
   /// whether or not to invoke \ref field_sensitivityt::apply
   bool run_apply = true;
 
+  const std::size_t max_field_sensitivity_array_size;
+
   void field_assignments_rec(
     const namespacet &ns,
     goto_symex_statet &state,
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 920b3b1e699..ab3c36bdbae 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -70,6 +70,9 @@ struct symex_configt final
   /// includes diagnostic information about call stack and guard size.
   bool show_symex_steps;
 
+  /// Maximum sizes for which field sensitivity will be applied to array cells
+  std::size_t max_field_sensitivity_array_size;
+
   /// \brief Construct a symex_configt using options specified in an
   /// \ref optionst
   explicit symex_configt(const optionst &options);
@@ -104,6 +107,7 @@ class goto_symext
     guard_managert &guard_manager)
     : should_pause_symex(false),
       symex_config(options),
+      field_sensitivity(symex_config.max_field_sensitivity_array_size),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table),
       guard_manager(guard_manager),
@@ -259,6 +263,9 @@ class goto_symext
   /// if we know the source language in use, irep_idt() otherwise.
   irep_idt language_mode;
 
+  /// Functor controling granularity of object accesses
+  field_sensitivityt field_sensitivity;
+
 protected:
   /// The symbol table associated with the goto-program being executed.
   /// This symbol table will not have objects that are dynamically created as
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index ffc43d3f409..84e40be36cc 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -34,10 +34,12 @@ static void get_l1_name(exprt &expr);
 
 goto_symex_statet::goto_symex_statet(
   const symex_targett::sourcet &_source,
+  field_sensitivityt &field_sensitivity,
   guard_managert &manager,
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
   : goto_statet(manager),
     source(_source),
+    field_sensitivity(field_sensitivity),
     guard_manager(manager),
     symex_target(nullptr),
     record_events({true}),
@@ -171,9 +173,15 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
 {
   // rename all the symbols with their last known value
 
+  static_assert(
+    level == L0 || level == L1 || level == L1_WITH_CONSTANT_PROPAGATION ||
+      level == L2,
+    "must handle all renaming levels");
+
   if(expr.id()==ID_symbol &&
      expr.get_bool(ID_C_SSA_symbol))
   {
+    exprt original_expr = expr;
     ssa_exprt &ssa=to_ssa_expr(expr);
 
     if(level == L0)
@@ -186,7 +194,7 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
       return renamedt<exprt, level>{
         std::move(rename_ssa<L1>(std::move(ssa), ns).value())};
     }
-    else if(level==L2)
+    else
     {
       ssa = set_indices<L1>(std::move(ssa), ns).get();
       rename<level>(expr.type(), ssa.get_identifier(), ns);
@@ -195,7 +203,14 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
       // renaming taken care of by l2_thread_encoding, or already at L2
       if(l2_thread_read_encoding(ssa, ns) || !ssa.get_level_2().empty())
       {
-        return renamedt<exprt, level>(std::move(ssa));
+        if(level == L1_WITH_CONSTANT_PROPAGATION)
+        {
+          // Don't actually rename to L2 -- we just used `ssa` to check whether
+          // constant-propagation was applicable
+          return renamedt<exprt, level>(std::move(original_expr));
+        }
+        else
+          return renamedt<exprt, level>(std::move(ssa));
       }
       else
       {
@@ -209,7 +224,8 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
         }
         else
         {
-          ssa = set_indices<L2>(std::move(ssa), ns).get();
+          if(level == L2)
+            ssa = set_indices<L2>(std::move(ssa), ns).get();
           return renamedt<exprt, level>(std::move(ssa));
         }
       }
@@ -261,6 +277,11 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
   }
 }
 
+// Explicitly instantiate the one version of this function without an explicit
+// caller in this file:
+template renamedt<exprt, L1_WITH_CONSTANT_PROPAGATION>
+goto_symex_statet::rename(exprt expr, const namespacet &ns);
+
 exprt goto_symex_statet::l2_rename_rvalues(exprt lvalue, const namespacet &ns)
 {
   rename(lvalue.type(), irep_idt(), ns);
@@ -351,7 +372,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
   }
 
   // only continue if an indivisible object is being accessed
-  if(field_sensitivityt::is_divisible(expr))
+  if(field_sensitivity.is_divisible(expr))
     return false;
 
   const ssa_exprt ssa_l1 = remove_level_2(expr);
@@ -479,7 +500,7 @@ goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared(
   }
 
   // only continue if an indivisible object is being accessed
-  if(field_sensitivityt::is_divisible(expr))
+  if(field_sensitivity.is_divisible(expr))
     return write_is_shared_resultt::NOT_SHARED;
 
   if(atomic_section_id != 0)
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index 7149ca8583f..4007a503657 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -47,6 +47,7 @@ class goto_symex_statet final : public goto_statet
 public:
   goto_symex_statet(
     const symex_targett::sourcet &,
+    field_sensitivityt &field_sensitivity,
     guard_managert &manager,
     std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
   ~goto_symex_statet();
@@ -67,6 +68,9 @@ class goto_symex_statet final : public goto_statet
   /// for error traces even after symbolic execution has finished.
   symbol_tablet symbol_table;
 
+  /// Reference to the functor, owned by goto_symext, used for renaming.
+  field_sensitivityt &field_sensitivity;
+
   // Manager is required to be able to resize the thread vector
   guard_managert &guard_manager;
   symex_target_equationt *symex_target;
@@ -120,8 +124,6 @@ class goto_symex_statet final : public goto_statet
     bool record_value,
     bool allow_pointer_unsoundness = false);
 
-  field_sensitivityt field_sensitivity;
-
 protected:
   template <levelt>
   void rename_address(exprt &expr, const namespacet &ns);
diff --git a/src/goto-symex/renamed.h b/src/goto-symex/renamed.h
index 58fe9ed9818..34bbc4e8188 100644
--- a/src/goto-symex/renamed.h
+++ b/src/goto-symex/renamed.h
@@ -16,7 +16,8 @@ enum levelt
 {
   L0 = 0,
   L1 = 1,
-  L2 = 2
+  L1_WITH_CONSTANT_PROPAGATION = 2,
+  L2 = 3
 };
 
 /// Wrapper for expressions or types which have been renamed up to a given
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 817affa9301..1160835ec17 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -204,7 +204,7 @@ void symex_assignt::assign_non_struct_symbol(
     current_assignment_type);
 
   const ssa_exprt &l1_lhs = assignment.lhs;
-  if(field_sensitivityt::is_divisible(l1_lhs))
+  if(state.field_sensitivity.is_divisible(l1_lhs))
   {
     // Split composite symbol lhs into its components
     state.field_sensitivity.field_assignments(
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 1db7524e09e..2f6d9da4dc6 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -394,6 +394,7 @@ void goto_symext::symex_printf(
   else
   {
     clean_expr(*va_args, state, false);
+    *va_args = field_sensitivity.apply(ns, state, *va_args, false);
     *va_args = state.rename(*va_args, ns).get();
     if(va_args->id() != ID_array)
     {
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index bef9746738f..af6c8a36c7b 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
+#include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
@@ -230,6 +231,18 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
     // (x == &o1 ? o1..field : o2..field). value_set_dereferencet can then
     // apply the dereference operation to each of o1..field and o2..field
     // independently, as it special-cases the ternary conditional operator.
+    // There may also be index operators in tmp1 which can now be resolved to
+    // constant array cell references, so we replace symbols with constants
+    // first, hoping for a transformation such as
+    // (x == &o1 ? o1 : o2)[idx] =>
+    // (x == &o1 ? o1 : o2)[2] =>
+    // (x == &o1 ? o1[[2]] : o2[[2]])
+    // Note we don't L2 rename non-constant symbols at this point, because the
+    // value-set works in terms of L1 names and we don't want to ask it to
+    // dereference an L2 pointer, which it would not have an entry for.
+
+    tmp1 = state.rename<L1_WITH_CONSTANT_PROPAGATION>(tmp1, ns).get();
+
     do_simplify(tmp1);
 
     if(symex_config.run_validation_checks)
@@ -241,7 +254,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
         "simplify re-introduced dereferencing");
     }
 
-    tmp1 = state.field_sensitivity.apply(ns, state, std::move(tmp1), write);
+    tmp1 = state.field_sensitivity.apply(ns, state, std::move(tmp1), false);
 
     // we need to set up some elaborate call-backs
     symex_dereference_statet symex_dereference_state(state, ns);
@@ -331,6 +344,20 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
   }
 }
 
+static exprt
+apply_to_objects_in_dereference(exprt e, const std::function<exprt(exprt)> &f)
+{
+  if(auto deref = expr_try_dynamic_cast<dereference_exprt>(e))
+  {
+    deref->op() = f(std::move(deref->op()));
+    return *deref;
+  }
+
+  for(auto &sub : e.operands())
+    sub = apply_to_objects_in_dereference(std::move(sub), f);
+  return e;
+}
+
 /// Replace all dereference operations within \p expr with explicit references
 /// to the objects they may refer to. For example, the expression `*p1 + *p2`
 /// might be rewritten to `obj1 + (p2 == &obj2 ? obj2 : obj3)` in the case where
@@ -370,19 +397,21 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
 ///    See \ref auto_objects.cpp for details.
 void goto_symext::dereference(exprt &expr, statet &state, bool write)
 {
-  // The expression needs to be renamed to level 1
-  // in order to distinguish addresses of local variables
-  // from different frames. Would be enough to rename
-  // symbols whose address is taken.
   PRECONDITION(!state.call_stack().empty());
-  exprt l1_expr = state.field_sensitivity.apply(
-    ns, state, state.rename<L1>(expr, ns).get(), write);
+
+  // Symbols whose address is taken need to be renamed to level 1
+  // in order to distinguish addresses of local variables
+  // from different frames.
+  expr = apply_to_objects_in_dereference(std::move(expr), [&](exprt e) {
+    return state.field_sensitivity.apply(
+      ns, state, state.rename<L1>(std::move(e), ns).get(), false);
+  });
 
   // start the recursion!
-  dereference_rec(l1_expr, state, write);
+  dereference_rec(expr, state, write);
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
-  expr = state.rename<L1>(std::move(l1_expr), ns).get();
+  expr = state.rename<L1>(std::move(expr), ns).get();
 
   // Dereferencing is likely to introduce new member-of-if constructs --
   // for example, "x->field" may have become "(x == &o1 ? o1 : o2).field."
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 535f2eefd23..6a1c5ab50ce 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -618,7 +618,7 @@ static void merge_names(
   }
 
   // field sensitivity: only merge on individual fields
-  if(field_sensitivityt::is_divisible(ssa))
+  if(dest_state.field_sensitivity.is_divisible(ssa))
     return;
 
   // shared variables are renamed on every access anyway, we don't need to
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index f2cd4c77a70..51e26804668 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -44,7 +44,14 @@ symex_configt::symex_configt(const optionst &options)
     partial_loops(options.get_bool_option("partial-loops")),
     debug_level(unsafe_string2int(options.get_option("debug-level"))),
     run_validation_checks(options.get_bool_option("validate-ssa-equation")),
-    show_symex_steps(options.get_bool_option("show-goto-symex-steps"))
+    show_symex_steps(options.get_bool_option("show-goto-symex-steps")),
+    max_field_sensitivity_array_size(
+      options.is_set("no-array-field-sensitivity")
+        ? 0
+        : options.is_set("max-field-sensitivity-array-size")
+            ? options.get_unsigned_int_option(
+                "max-field-sensitivity-array-size")
+            : DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE)
 {
 }
 
@@ -347,6 +354,7 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
   // create and prepare the state
   auto state = util_make_unique<statet>(
     symex_targett::sourcet(entry_point_id, start_function->body),
+    field_sensitivity,
     guard_manager,
     [storage](const irep_idt &id) { return storage->get_unique_l2_index(id); });
 
diff --git a/src/util/magic.h b/src/util/magic.h
index 2f086f6cbff..5fb4d986a4b 100644
--- a/src/util/magic.h
+++ b/src/util/magic.h
@@ -16,4 +16,8 @@ const std::size_t MAX_CONCRETE_STRING_SIZE = 1 << 26;
 // The top end of the range of integers for which dstrings are precomputed
 constexpr std::size_t DSTRING_NUMBERS_MAX = 64;
 
+/// Limit the size of arrays for which field_sensitivity gets applied.
+/// Necessary because large constant arrays slow-down the process.
+constexpr std::size_t DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE = 64;
+
 #endif
diff --git a/unit/goto-symex/goto_symex_state.cpp b/unit/goto-symex/goto_symex_state.cpp
index 46858ce15ad..bb310223568 100644
--- a/unit/goto-symex/goto_symex_state.cpp
+++ b/unit/goto-symex/goto_symex_state.cpp
@@ -35,12 +35,14 @@ SCENARIO(
   // Initialize goto state
   std::list<goto_programt::instructiont> target;
   symex_targett::sourcet source{"fun", target.begin()};
+  field_sensitivityt field_sensitivity{
+    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE};
   guard_managert manager;
   std::size_t fresh_name_count = 1;
   auto fresh_name = [&fresh_name_count](const irep_idt &) {
     return fresh_name_count++;
   };
-  goto_symex_statet state{source, manager, fresh_name};
+  goto_symex_statet state{source, field_sensitivity, manager, fresh_name};
 
   // Initialize dirty field of state
   incremental_dirtyt dirty;
diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp
index ffa69c1b772..3615d9538d2 100644
--- a/unit/goto-symex/symex_assign.cpp
+++ b/unit/goto-symex/symex_assign.cpp
@@ -43,12 +43,14 @@ SCENARIO(
   // Initialize goto state
   std::list<goto_programt::instructiont> target;
   symex_targett::sourcet source{"fun", target.begin()};
+  field_sensitivityt field_sensitivity{
+    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE};
   guard_managert manager;
   std::size_t fresh_name_count = 1;
   auto fresh_name = [&fresh_name_count](const irep_idt &) {
     return fresh_name_count++;
   };
-  goto_symex_statet state{source, manager, fresh_name};
+  goto_symex_statet state{source, field_sensitivity, manager, fresh_name};
 
   // Initialize dirty field of state
   incremental_dirtyt dirty;
diff --git a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp
index 60b7aa47432..3955740c6ad 100644
--- a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp
+++ b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp
@@ -52,10 +52,12 @@ SCENARIO(
   // Initialize goto state
   std::list<goto_programt::instructiont> target;
   symex_targett::sourcet source{"fun", target.begin()};
+  field_sensitivityt field_sensitivity{
+    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE};
   guard_managert guard_manager;
   std::size_t count = 0;
   auto fresh_name = [&count](const irep_idt &) { return count++; };
-  goto_symex_statet state{source, guard_manager, fresh_name};
+  goto_symex_statet state{source, field_sensitivity, guard_manager, fresh_name};
 
   GIVEN("A value set in which pointer symbol `ptr1` only points to `&value1`")
   {
@@ -246,7 +248,6 @@ SCENARIO(
 
     // struct_symbol..pointer_field <- &value1
     {
-      field_sensitivityt field_sensitivity;
       const exprt index_fs =
         field_sensitivity.apply(ns, state, member_l1.get(), true);
       value_set.assign(index_fs, address1_l1.get(), ns, false, false);